List of theorems referencing the symbol SIGMA_THRYVAR

(515) Theorem sigma_theory0: [Recursive formula for generalized sum] (FORALL x | Finite(x) •imp (sigma_thryvar(x) = if x = 0 then e else pluz(sigma_thryvar(x - {arb(x)}),cdr(arb(x))) end if))
(516) Theorem sigma_theory1: [Summation of null map is zero] sigma_thryvar(0) = e
(517) Theorem sigma_theory2: [Summation of singleton map is range element] (cdr(X) in s) •imp (sigma_thryvar({X}) = cdr(X))
(517+) Theorem sigma_theory3: [Sum value belongs to closed range of map] (Finite(F) & (range(F) •incin s)) •imp (sigma_thryvar(F) in s)
(518) Theorem sigma_theory4: [Removal of single element from domain of a sum] ((C in F) & Finite(F) & (range(F) •incin s)) •imp (sigma_thryvar(F) = pluz(sigma_thryvar(F - {C}),cdr(C)))
(519) Theorem sigma_theory5: [The generalized sum of a union map is a sum of sums] (Finite(F) & Is_map(F) & (range(F) •incin s)) •imp (sigma_thryvar(F) = pluz(sigma_thryvar(F •ON (domain(F) * T)), sigma_thryvar(F •ON (domain(F) - T))))
(520) Theorem sigma_theory6: [Rearrangement-of-sums theorem] (Finite(F) & Svm(F) & Svm(G) & (domain(F) = domain(G)) & (range(F) •incin s)) •imp (sigma_thryvar(F) = sigma_thryvar({[y,sigma_thryvar(F •ON (G •INV_IM {y}))]: y in range(G)}))
(520+) Theorem sigma_theory7: [Sum permutation theorem] (Finite(F) & Svm(F) & one_1_map(G) & (domain(F) = domain(G)) & (range(F) •incin s)) •imp (sigma_thryvar(F) = sigma_thryvar({[y,F~[inv(G)~[y]]]: y in range(G)}))