List of theorems referencing the symbol DOT_ON

(69) Theorem 48: [Map restriction lemma] (F •ON A) •incin F
(77) Theorem 56: [Map restrictions are maps] Is_map(F) •imp Is_map(F •ON S)
(78) Theorem 57: [Restrictions of single-valed maps are single-valued] Svm(F) •imp Svm(F •ON S)
(79) Theorem 58: [Restrictions of one-one maps are one-one] one_1_map(F) •imp one_1_map(F •ON S)
(84) Theorem 63: [Map restriction is additive] F •ON (A + B) = (F •ON A) + (F •ON B)
(85) Theorem 64: [Restriction of union maps] (F + G) •ON A = (F •ON A) + (G •ON A)
(88) Theorem 67: [Restriction of a map to its own domain] F •ON domain(F) = F
(89) Theorem 68: [Restriction to an intersection set] F •ON (domain(F) * T) = F •ON T
(90) Theorem 69: [Double restriction] F •ON (S * T) = (F •ON S) •ON T
(91) Theorem 70: [Null restriction] F •ON 0 = 0
(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)
(125) Theorem 93: [Domain of restriction] domain(F •ON S) = domain(F) * S
(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)))
(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)))
(150) Theorem 111: [Composition with an identity map is restriction] (Is_map(F)) •imp (F @ ident(S) = F •ON S)
(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}))
(159) Theorem 120: [Value of a restriction map] (F •ON S)~[X] = if X in domain(F •ON S) then F~[X] else 0 end if
(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)}))
(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))
(209) Theorem 170: [Cardinality of restriction maps] (Svm(F) & (domain(F) incs A)) •imp (#(F •ON A) = #A)
(215) Theorem 175: [Range of a restricted inverse map] G •INV_IM R = range(inv(G) •ON R)
(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)
(220) Theorem 180: [Inverse images by a single-valued map] Svm(G) •imp ((G •ON (G •INV_IM A)) •INV_IM B = (G •INV_IM A) * (G •INV_IM B))
(222) Theorem 182: [Successive map restrictions] (((F •ON A) •ON B) = (F •ON (A * B)))
(380) Theorem 329: ((F in Fin_seqs(S)) & (M in Za)) •imp (((F •ON M) in Fin_seqs(S)) & (shifted_seq(F,M) in Fin_seqs(S)) & (domain(shifted_seq(F,M)) = (#F •MINUS M)))
(384) Theorem 333: [Concatenation of shifted sequences] ((F in Fin_seqs(S)) & (M in domain(F))) •imp ((shifted_seq(F,M) in Fin_seqs(S)) & (F = concat((F •ON M), shifted_seq(F,M))))
(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))))
(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)}))
(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)))))
(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))))))
(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)})))
(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)))