List of theorems referencing the symbol range

(38) Theorem 25: [Only the null set has a null range] (S = 0) •eq (range(S) = 0)
(40) Theorem iz_map.1: [Mapformers are maps] Is_map({[a(x),b(x)]: x in s}) & (domain({[a(x),b(x)]: x in s}) = {a(x): x in s}) & (range({[a(x),b(x)]: x in s}) = {b(x): x in s})
(80) Theorem 59: [The null set as a map] Is_map(0) & Svm(0) & (one_1_map(0)) & (range(0) = 0) & (domain(0) = 0)
(82) Theorem 61: [Range membership lemma] (X in F) •imp (cdr(X) in range(F))
(86) Theorem 65: [Monotonicity of range and domain sets] (F •incin G) •imp ((range(F) •incin range(G)) & (domain(F) •incin domain(G)))
(92) Theorem 71: [Map image elements belong to the map range] (X in domain(F)) •imp ((F~[X]) in range(F))
(99) Theorem fcn_symbol.5: [Range of a mapformer] range(g) = {f(xx) : xx in s}
(103) Theorem 73: [Form of a single-valued map range] Svm(F) •imp (F = {[x,F~[x]]: x in domain(F)} & (range(F) = {F~[x]: x in domain(F)}))
(105) Theorem 75: (X in domain(F)) •imp (F~[X] in range(F))
(108) Theorem Must_be_svm.1: [Single-valued map former] Svm({[x,b(x)]: x in s}) & (domain({[x,b(x)]: x in s}) = s) & (range({[x,b(x)]: x in s}) = {b(x): x in s}) & ((u in s) •imp ({[x,b(x)]: x in s}~[u] = b(u)))
(111) Theorem 79: [Map ranges are additive] range(F + G) = range(F) + range(G)
(112) Theorem 80: [Range of a restriction map] range(F •ON S) •incin range(F)
(113) Theorem 81: [Range of restriction to a union] range(F •ON (S + T)) = range(F •ON S) + range(F •ON T)
(114) Theorem 82: [Restriction to a subset] (S incs T) •imp (range(F •ON S) incs range(F •ON T))
(115) Theorem 83: [One-one map-restriction to an intersection] one_1_map(F) •imp (range(F •ON (S * T)) = range(F •ON S) * range(F •ON T))
(116) Theorem 84: [Restriction to the null set] ((F •ON 0) = 0) & (range(F •ON 0) = 0)
(117) Theorem 85: [One-one map restriction to disjoint sets] (one_1_map(F) & (S * T = 0)) •imp (range(F •ON S) * range(F •ON T) = 0)
(118) Theorem 86: [Domain is null only when range is null] (domain(F) = 0) •eq (range(F) = 0)
(120) Theorem 88: [Union of 1-1 maps] (one_1_map(F) & one_1_map(G) & (range(F) * range(G) = 0) & (domain(F) * domain(G) = 0)) •imp one_1_map(F + G)
(121) Theorem 89: [Union of 1-1 maps, 2] (one_1_map(F + G) & ((G * F) = 0)) •imp ((domain(G) = (domain(F + G) - domain(F))) & (range(G) = (range(F + G) - range(F))))
(126) Theorem 94: [Range and domain of map product] (range(F @ G) = range(F •ON range(G))) & ((range(G) •incin domain(F)) •imp (domain(F @ G) = domain(G)))
(127) Theorem 95: [Range and domain of map product, 2] (range(G) = domain(F)) •imp ((range(F @ G) = range(F)) & (domain(F @ G) = domain(G)))
(128) Theorem 96: [Range and domain of map product, 3] (range(G) •incin domain(F)) •imp ((range(F @ G) •incin range(F)) & (domain(F @ G) = domain(G)))
(129) Theorem 97: [Range of restriction of one-one map] (one_1_map(F) & (S •incin domain(F)) & (S /= domain(F))) •imp ((range(F •ON S) •incin range(F)) & (range(F •ON S) /= range(F)))
(130) Theorem 98: [Inverse map basic properties] Is_map(inv(F)) & range(inv(F)) = domain(F) & domain(inv(F)) = range(F)
(132) Theorem 100: [Inverse of a one-one map] one_1_map(F) •imp (one_1_map(inv(F)) & (F = inv(inv(F))) & (range(inv(F)) = domain(F)) & (domain(inv(F)) = range(F)))
(134) Theorem 102: [Inverse image of an element's map image] one_1_map(F) •imp (((X in domain(F)) •imp (inv(F)~[F~[X]] = X)) & ((X in range(F)) •imp (F~[inv(F)~[X]] = X)))
(146) Theorem 107: [Range formation and unionset formation commute] range(Un(S)) = Un({range(f): f in S})
(148) Theorem 109: [Domain and range of singleton and doubleton maps] (domain({[X,Y]}) = {X}) & (range({[X,Y]}) = {Y}) & (domain({[X,Y],[U,V]}) = {X,U}) & (range({[X,Y],[U,V]}) = {Y,V})
(149) Theorem 110: [Elementary properties of identity maps] one_1_map(ident(S)) & (domain(ident(S)) = S) & (range(ident(S)) = S) & (inv(ident(S)) = ident(S)) & ((X in S) •imp (ident(S)~[X] = X)) & (Is_map(F) •imp (((domain(F) •incin S) •imp (F @ ident(S) = F)) & ((range(F) •incin S) •imp (ident(S) @ F = F))))
(151) Theorem 112: [Composition with the inverse map] Svm(F) •imp (F @ inv(F) = ident(range(F)))
(152) Theorem 113: [Inverses of one-one maps] one_1_map(F) •imp (((F @ inv(F)) = ident(range(F))) & ((inv(F) @ F) = ident(domain(F))))
(153) Theorem 114: [Product of inverses lemma] (Is_map(F) & Is_map(G) & (domain(F) •incin range(G)) & Svm(F @ G)) •imp Svm(F)
(156) Theorem 117: [An inverse pair of maps must be 1-1 and must be each other's inverses] (Is_map(F) & Is_map(G) & (domain(F) = range(G)) & (range(F) = domain(G)) & (F @ G = ident(range(F))) & (G @ F = ident(domain(F)))) •imp (one_1_map(F) & (G = inv(F)))
(157) Theorem 118: [Single-valued map restrictions as setformers] Svm(F) •imp (((F •ON S) = {[x,F~[x]]: x in domain(F) | x in S}) & (domain(F •ON S) = {x: x in domain(F) | x in S}) & (range(F •ON S) = {F~[x]: x in domain(F) | x in S}))
(160) Theorem 121: [Single-valued map restrictions as setformers, 2] Svm(F) •imp (((F •ON S) = {[x,F~[x]]: x in domain(F •ON S)}) & (range(F •ON S) = {F~[x]: x in domain(F •ON S)}))
(163) Theorem 124: [Images under single-valued map composition] (Svm(F) & Svm(G) & (X in domain(G)) & (range(G) •incin domain(F))) •imp ((F @ G)~[X] = F~[G~[X]])
(164) Theorem 125: [Single-valued map ranges and domains as set formers] (Svm(F) & Svm(G) & (X in domain(G)) & (range(G) •incin domain(F))) •imp (((F @ G)~[X] = F~[G~[X]]) & (F @ G = {[x,F~[G~[x]]]: x in domain(G)}) & (range(F @ G) = {F~[G~[x]]: x in domain(G)}))
(169) Theorem 130: [A 1-1 map on a set u induces a 1-1 map on the power set of u] (one_1_map(F) & (S •incin domain(F)) & (T •incin domain(F)) & (S /= T)) •imp (range(F •ON S) /= range(F •ON T))
(172) Theorem 133: [Single-valued maps have 1-1 partial inverses] Svm(F) •imp (EXISTS h | ((domain(h) = range(F)) & (range(h) •incin domain(F)) & one_1_map(h)) & (FORALL x in range(F) | (F~[h~[x]] = x)))
(175) Theorem 136: [Subsets of Cartesian products] (Y •incin (S •PROD T)) •eq (Is_map(Y) & (domain(Y) •incin S) & (range(Y) •incin T))
(178) Theorem 139: [Cartesian modified associativity] (F = {[[[x,y],z],[x,[y,z]]]: x in A, y in B, z in C}) •imp (one_1_map(F) & (domain(F) = ((A •PROD B) •PROD C)) & (range(F) = (A •PROD (B •PROD C))))
(179) Theorem 140: [Cartesian modified commutativity] (F = {[[x,y],[y,x]]: x in A, y in B}) •imp (one_1_map(F) & (domain(F) = (A •PROD B)) & (range(F) = (B •PROD A)))
(181) Theorem 142: [Cardinality lemma] Ord(#S) & (EXISTS f in OM | (one_1_map(f) & (range(f) = S) & (domain(f) = #S))) & (not((EXISTS o in #S | (EXISTS g in OM | one_1_map(g) & (range(g) = S) & (domain(g) = o)))))
(189) Theorem 150: [Enumerability lemma] (Ord(S) & (T •incin S)) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (domain(f) •incin S) & (range(f) = T))
(190) Theorem 151: [Cardinality theorem] Card(#S) & Ord(#S) & (EXISTS f in OM | one_1_map(f) & (range(f) = S) & (domain(f) = #S))
(191) Theorem 152: [One-one maps are cardinality preserving] one_1_map(F) •imp (#range(F) = #domain(F))
(192) Theorem 153: [Equicardinality is equivalent to one-one correspondence] (EXISTS F in OM | (one_1_map(F) & (range(F) = S) & (domain(F) = T))) •eq (#S = #T)
(199) Theorem 160: [Uniqueness of Cardinality] (Card(C) & (EXISTS f in OM | (one_1_map(f) & (range(f) = S) & domain(f) = C))) •imp (C = #S)
(205) Theorem 166: [Single-valued mapping cannot increase cardinality] Svm(F) •imp (#range(F) •incin #domain(F))
(207) Theorem 168: [The cardinality of a map is no smaller than the cardinality of its range] #range(F) •incin #F
(211) Theorem 171: [Condition for existence of a single-valued map between two sets] (#S incs #T) •eq (T = 0 or (EXISTS f in OM | Svm(f) & (domain(f) = S) & (range(f) = T)))
(212) Theorem 172: [Domains and ranges of inverse] domain(G) = (G •INV_IM R) + (G •INV_IM (range(G) - R))
(214) Theorem 174: [Inverse image of a range element] (Y in range(G)) •imp ((G •INV_IM {Y}) /= 0)
(215) Theorem 175: [Range of a restricted inverse map] G •INV_IM R = range(inv(G) •ON R)
(216) Theorem 176: [Single-valued inverse image as a setformer] Svm(inv(G)) •imp (G •INV_IM R = {inv(G)~[w]: w in (R * range(G))})
(217) Theorem 177: [Inverse image of a range element] (one_1_map(G) & (Y in range(G))) •imp (G •INV_IM {Y} = {inv(G)~[Y]})
(218) Theorem 178: [Range of a map restricted to an inverse image] range(G •ON (G •INV_IM R)) incs (range(G) * R)
(219) Theorem 179: [Range of a single-valued map restricted to an inverse image] Svm(G) •imp (range(G •ON (G •INV_IM A)) = range(G) * A)
(225) Theorem 185: [One-one maps preserve finiteness] one_1_map(F) •imp ((Finite(domain(F))) •imp (Finite(range(F))))
(226) Theorem 186: [One-one maps preserve finiteness, 2] one_1_map(F) •imp (Finite(domain(F)) •eq Finite(range(F)))
(227) Theorem 187: [A single_valued map with finite domain has a finite range] (Svm(F) & Finite(domain(F))) •imp Finite(range(F))
(231) Theorem 190: [A set is finite if and only if it is not the single-valued image of any of its finite subsets] Finite(S) •eq (not(EXISTS f in OM | (Svm(f) & (range(f) = S) & (domain(f) •incin S) & (S /= domain(f)))))
(234) Theorem 193: [Interchange lemma] ((X in S) & (Y in S)) •imp (EXISTS f | one_1_map(f) & (range(f) = S) & (domain(f) = S) & ((f~[X]) = Y) & ((f~[Y]) = X))
(369) Theorem 318: [Finite sequences are single_valued maps with integer domains] (F in Fin_seqs(S)) •eq (Svm(F) & (domain(F) in Za) & (range(F) •incin S))
(373) Theorem 322: [The shift-map of an integer is single-valued and maps Za into Za] ((M in Za) & (N in Za)) •imp (Svm(Shift(M)) & (domain(Shift(M)) = Za) & (range(Shift(M)) •incin Za) & (Shift(M)~[N] = M •PLUS N))
(381) Theorem 330: [Concatenation of finite sequences] ((F in Fin_seqs(S)) & (G in Fin_seqs(S))) •imp ((concat(F,G) in Fin_seqs(S)) & (domain(concat(F,G)) = domain(F) •PLUS domain(G)) & (range(concat(F,G)) = range(F) + range(G))) & ((U in domain(F) •PLUS domain(G)) •imp (concat(F,G)~[U] = if U in domain(F) then F~[U] else G~[U •MINUS domain(F)] end if))
(385) Theorem subseq.1: (g = (f @ h_thryvar)) & one_1_map(h_thryvar) & (domain(h_thryvar) in next(Za)) & (range(h_thryvar) •incin domain(f)) & (FORALL i in domain(h_thryvar), j in domain(h_thryvar) | (i in j) •imp ((h_thryvar~[i]) in (h_thryvar~[j])))
(387) Theorem subseq.3: Svm(g) & (g •incin (domain(f) •PROD range(f))) & (domain(g) in (next(Za) * next(domain(f))))
(424) Theorem well_ordered_set.9: (Ord(V) & (ordenm_thryvar(V) /= s)) •imp ( one_1_map({[x,ordenm_thryvar(x)]: x in V}) & (domain({[x,ordenm_thryvar(x)]: x in V}) = V) & (range({[x,ordenm_thryvar(x)]: x in V}) = {u: u in s | arg1_bef_arg2(u,ordenm_thryvar(V))}) & ({u: u in s | arg1_bef_arg2(u,ordenm_thryvar(V))} = {ordenm_thryvar(x): x in V}))
(436) Theorem 343: (Ord(O1) & Ord(O2)) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f), y in domain(f) | (x in y) •eq (((car(f~[x]) + cdr(f~[x])) in (car(f~[y]) + cdr(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) in car(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) = car(f~[y])) & (cdr(f~[x]) in cdr(f~[y]))))))
(437) Theorem 344: (Card(O1) & Card(O2) & (not Finite(O1 + O2))) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f) | (EXISTS y in (O1 + O2) | range(f •ON x) •incin (y •PROD y))))
(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)}))
(533) Theorem linear_order_12: (FORALL f | (Finite(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) in next(s0))) & (FORALL x | (cdr(x) in next(s0)) •imp (min_over_thryvar({x}) = cdr(x))) & (FORALL f,t | (Finite(f) & Is_map(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) = smaller_thryvar(min_over_thryvar(f •ON (domain(f) * t)),min_over_thryvar(f •ON (domain(f) - t))))) & (FORALL c,f | ((c in f) & Finite(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) = smaller_thryvar(min_over_thryvar(f - {c}),cdr(c))))
(534) Theorem linear_order_13: (Svm(F) & (range(F) •incin s0) & Finite(F)) •imp (((P in F) •imp (min_over_thryvar({P}) = (F~[car(P)]))) & (min_over_thryvar(F) = smaller_thryvar(min_over_thryvar(F •ON (domain(F) * A)),min_over_thryvar(F •ON (domain(F) - A)))))
(535) Theorem linear_order_14: (Svm(F) & (range(F) •incin s0) & Finite(F) & (F /= 0)) •imp (min_over_thryvar(F) in range(F))
(541) Theorem linear_order_20: (FORALL x, y | larger_thryvar(x,y) = if ((x notin s0) & (y notin s0)) then s0 elseif (x notin s0) then y elseif (y notin s0) then x elseif arg1_aft_arg2(x,y) then x else y end if) & (FORALL x, y | larger_thryvar(x,y) = larger_thryvar(y,x)) & (FORALL x, y | ({x,y} •incin s0) •imp (larger_thryvar(x,y) in {x,y})) & (FORALL x | (x in next(s0)) •imp (larger_thryvar(x,s0) = x)) & (FORALL x, y, z | larger_thryvar(x,larger_thryvar(y,z)) = larger_thryvar(larger_thryvar(x,y),z)) & (FORALL x, y | ((x in next(s0)) & (y in next(s0))) •imp (larger_thryvar(x,y) in next(s0))) & (FORALL f,p,a | (Svm(f) & (range(f) •incin s0) & Finite(f)) •imp (((p in f) •imp (max_over_thryvar({p}) = (f~[car(p)]))) & (max_over_thryvar(f) = larger_thryvar(max_over_thryvar(f •ON (domain(f) * a)),max_over_thryvar(f •ON (domain(f) - a)))))) & (FORALL f | (Svm(f) & (range(f) •incin s0) & Finite(f) & (f /= 0)) •imp (max_over_thryvar(f) in range(f))) & (FORALL x, y | ({x,y} •incin s0) •imp ((larger_thryvar(x,y) = x) •eq (arg1_aft_arg2(x,y) or (x = y)))) & (FORALL t | lbs_thryvar(t) = {x in s0 | (FORALL y in (t * s0) | larger_thryvar(y,x) = y)}) & (FORALL t | min_thryvar(t) = arb({s0} + (t * lbs_thryvar(t)))) & (FORALL t | glb_thryvar(t) = arb({s0} + {x in lbs_thryvar(t) | lbs_thryvar(t) •incin lbs_thryvar({x})})) & (lbs_thryvar(0) = s0) & (min_thryvar(0) = s0) & (FORALL t | (lbs_thryvar(t) •incin s0) & (lbs_thryvar(t) = lbs_thryvar(t * s0)) & (min_thryvar(t) = min_thryvar(t * s0))) & (FORALL t, x | (Finite(t) & (x in t) & (t •incin s0)) •imp ((min_thryvar(t) in t) & ((x = min_thryvar(t)) or (arg1_aft_arg2(x,min_thryvar(t))))))
(643) Theorem 496: (FORALL x, y | smaller_Ra(x,y) = if ((x notin Ra) & (y notin Ra)) then Ra elseif (x notin Ra) then y elseif (y notin Ra) then x elseif (x •Ra_LT y) then x else y end if) & (FORALL x, y | smaller_Ra(x,y) = smaller_Ra(y,x)) & (FORALL x, y | ({x,y} •incin Ra) •imp (smaller_Ra(x,y) in {x,y})) & (FORALL x | (x in next(Ra)) •imp (smaller_Ra(x,Ra) = x)) & (FORALL x, y, z | smaller_Ra(x,smaller_Ra(y,z)) = smaller_Ra(smaller_Ra(x,y),z)) & (FORALL x, y | ((x in next(Ra)) & (y in next(Ra))) •imp (smaller_Ra(x,y) in next(Ra))) & (FORALL f,p,a | (Svm(f) & (range(f) •incin Ra) & Finite(f)) •imp (((p in f) •imp (min_over_Ra({p}) = (f~[car(p)]))) & (min_over_Ra(f) = smaller_Ra(min_over_Ra(f •ON (domain(f) * a)),min_over_Ra(f •ON (domain(f) - a)))))) & (FORALL f | (Svm(f) & (range(f) •incin Ra) & Finite(f) & (f /= 0)) •imp (min_over_Ra(f) in range(f))) & (FORALL x, y | ({x,y} •incin Ra) •imp ((smaller_Ra(x,y) = x) •eq ((x •Ra_LT y) or (x = y)))) & (FORALL t | ubs_Ra(t) = {x in Ra | (FORALL y in (t * Ra) | smaller_Ra(y,x) = y)}) & (FORALL t | max_Ra(t) = arb({Ra} + (t * ubs_Ra(t)))) & (FORALL t | lub_Ra(t) = arb({Ra} + {x in ubs_Ra(t) | ubs_Ra(t) •incin ubs_Ra({x})})) & (ubs_Ra(0) = Ra) & (max_Ra(0) = Ra) & (FORALL t | (ubs_Ra(t) •incin Ra) & (ubs_Ra(t) = ubs_Ra(t * Ra)) & (max_Ra(t) = max_Ra(t * Ra))) & (FORALL t, x | (Finite(t) & (x in t) & (t •incin Ra)) •imp ((max_Ra(t) in t) & ((x = max_Ra(t)) or ((x •Ra_LT max_Ra(t))))))
(667) Theorem 521: [The range of a rational sequence is included in the set of rationals] (F in RaSeq) •imp ((domain(F) = Za) & (range(F) •incin Ra) & ((X in Za) •imp (F~[X] in Ra)))
(671) Theorem pointwiseU.2: Svm(h) & (domain(h) = d) & (range(h) •incin r)
(674) Theorem pointwise.2: Svm(h) & (domain(h) = d) & (range(h) •incin r)
(678) Theorem 527: (F in RaSeq) •imp ((domain(F) = Za) & Svm(F) & (range(F) •incin Ra) & Ra_eqseq(F,F))
(691) Theorem 540: [Every Cauchy sequence has an upper bound] (F in RaCauchy) •imp (EXISTS x in Ra | (FORALL y in range(F) | y •Ra_LE x))
(692) Theorem 541: (F in RaCauchy) •imp (EXISTS x in Ra | (FORALL y in range(F) | Ra_ABS(y) •Ra_LT x ))
(900) Theorem 745: (R_SIGMA(0) = R_0) & (FORALL x in OM | (cdr(x) in Re) •imp (R_SIGMA({x}) = cdr(x))) & (FORALL f in OM | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) in Re)) & (FORALL f in OM, c in f | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA(f - {c}) •R_PLUS cdr(c))) & (FORALL f in OM | (Finite(f) & Is_map(f) & (range(f) •incin Re)) •imp (FORALL t | R_SIGMA(f) = R_SIGMA(f •ON (domain(f) * t)) •R_PLUS R_SIGMA(f •ON (domain(f) - t)))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & Svm(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,R_SIGMA(f •ON (g •INV_IM {y}))]: y in range(g)}))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & one_1_map(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,f~[inv(g)~[y]]]: y in range(g)})))
(901) Theorem 746: (R_SIGMA(0) = R_0) & ((cdr(X) in Re) •imp (R_SIGMA({X}) = cdr(X))) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) in Re)) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA(F - {c}) •R_PLUS cdr(c))) & ((Finite(F) & Is_map(F) & (range(F) •incin Re)) •imp R_SIGMA(F) = R_SIGMA(F •ON (domain(F) * T)) •R_PLUS R_SIGMA(F •ON (domain(F) - T))) & ((Finite(F) & Svm(F) & Svm(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,R_SIGMA(F •ON (G •INV_IM {y}))]: y in range(G)}))) & ((Finite(F) & Svm(F) & one_1_map(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,F~[inv(G)~[y]]]: y in range(G)})))
(904) Theorem 749: [Continuous functions map limits into limits] (Cf_RR(F,S) & (G in ReCauchy) & (range(G) •incin S)) •imp ((F @ G in ReCauchy) & (limit(F @ G) = F~[limit(G)]))
(907) Theorem 752: [The composition of two real continuous functions is continuous.] (Cf_RR(F,S) & Cf_RR(G,T) & (range(G •ON T) •incin S)) •imp Cf_RR(F @ G,T)
(913) Theorem 758: (Cf_RR(F,I(X,Y)) & (X in Re) & (Y in Re)) •imp (EXISTS u in I(X,Y), v in I(X,Y) | range(F •ON I(X,Y)) = I(f~[u],f~[v]))
(947) Theorem real_sigma0: (FORALL f | (Finite(f) & (range(f) •incin Re)) •imp (Sig(f) in Re)) & (FORALL x | (cdr(x) in Re) •imp (Sig({x}) = cdr(x))) & (FORALL f,t | (Finite(f) & Is_map(f) & (range(f) •incin Re)) •imp (Sig(f) = (Sig(f •ON (domain(f) * t)) •R_PLUS Sig(f •ON (domain(f) - t)))))
(948) Theorem real_sigma: (Svm(F) & (range(F) •incin Re) & Finite(F)) •imp ((Sig(F) in Re) & ((P in F) •imp (Sig({P}) = (F~[car(P)]))) & (Sig(F) = (Sig(F •ON (domain(F) * A)) •R_PLUS Sig(F •ON (domain(F) - A)))))
(955) Theorem real_function_sigma: (Svm(ser) & (range(ser) •incin RF) & Finite(ser)) •imp ((FSig(ser) in RF & (p in ser) •imp (Sig({p}) = ser(car(p)))) &(FORALL a | Sig(ser) = Sig(ser •ON (domain(ser) * a)) •R_PLUS Sig(ser •ON domain(ser) - a)))