= 0 proof A1: n in NAT by ORDINAL1:def 12; dom (P * ASeq) = NAT by SEQ_1:1; then (P * ASeq).n = P.(ASeq.n) by A1,FUNCT_1:12; hence thesis by PROB_1:def 8; end; theorem Th5: ASeq.n c= BSeq.n implies (P * ASeq).n <= (P * BSeq).n proof A1: n in NAT by ORDINAL1:def 12; assume ASeq.n c= BSeq.n; then P.(ASeq.n) <= P.(BSeq.n) by PROB_1:34; then (P * ASeq).n <= P.(BSeq.n) by A1,FUNCT_2:15; hence thesis by A1,FUNCT_2:15; end; theorem Th6: ASeq is non-descending implies P * ASeq is non-decreasing proof A1: dom (P * ASeq) = NAT by SEQ_1:1; assume A2: ASeq is non-descending; now let n,m be Nat; assume n <= m; then A3: ASeq.n c= ASeq.m by A2,PROB_1:def 5; reconsider nn=n, mm=m as Element of NAT by ORDINAL1:def 12; (P * ASeq).nn = P.(ASeq.nn) & (P * ASeq).mm = P.(ASeq.mm) by A1,FUNCT_1:12; hence (P * ASeq).n <= (P * ASeq).m by A3,PROB_1:34; end; hence thesis by SEQM_3:6; end; theorem Th7: ASeq is non-ascending implies P * ASeq is non-increasing proof A1: dom (P * ASeq) = NAT by SEQ_1:1; assume A2: ASeq is non-ascending; now let n,m be Nat; assume n <= m; then A3: ASeq.m c= ASeq.n by A2,PROB_1:def 4; reconsider nn=n, mm=m as Element of NAT by ORDINAL1:def 12; (P * ASeq).nn = P.(ASeq.nn) & (P * ASeq).mm = P.(ASeq.mm) by A1,FUNCT_1:12; hence (P * ASeq).m <= (P * ASeq).n by A3,PROB_1:34; end; hence thesis by SEQM_3:8; end; definition let X be set, A1 be SetSequence of X; func Partial_Intersection A1 -> SetSequence of X means :Def1: it.0 = A1.0 & for n being Nat holds it.(n+1) = it.n /\ A1.(n+1); existence proof defpred P[set,set,set] means for x,y being Subset of X,s being Nat holds s = $1 & x = $2 & y = $3 implies y = x /\ A1.(s+1); A1: for n being Nat for x being Subset of X ex y being Subset of X st P[n,x,y] proof let n be Nat; let x be Subset of X; take x /\ A1.(n+1); thus thesis; end; consider F being SetSequence of X such that A2: F.0 = A1.0 and A3: for n being Nat holds P[n,F.n,F.(n+1)] from RECDEF_1:sch 2(A1 ); take F; thus F.0 = A1.0 by A2; let n be Nat; reconsider n as Element of NAT by ORDINAL1:def 12; P[n,F.n,F.(n+1)] by A3; hence thesis; end; uniqueness proof let S1,S2 be SetSequence of X such that A4: S1.0 = A1.0 and A5: for n being Nat holds S1.(n+1) = S1.n /\ A1.(n+1) and A6: S2.0 = A1.0 and A7: for n being Nat holds S2.(n+1) = S2.n /\ A1.(n+1); defpred P[object] means S1.$1 = S2.$1; for n being object holds n in NAT implies P[n] proof let n be object; assume n in NAT; then reconsider n as Element of NAT; A8: for k st P[k] holds P[k+1] proof let k; assume S1.k = S2.k; hence S1.(k+1) = S2.k /\ A1.(k+1) by A5 .= S2.(k+1) by A7; end; A9: P[0] by A4,A6; for k being Nat holds P[k] from NAT_1:sch 2(A9,A8); then S1.n = S2.n; hence thesis; end; hence thesis; end; end; definition let X be set, A1 be SetSequence of X; func Partial_Union A1 -> SetSequence of X means :Def2: it.0 = A1.0 & for n being Nat holds it.(n+1) = it.n \/ A1.(n+1); existence proof defpred P[set,set,set] means for x,y being Subset of X,s being Nat holds (s = $1 & x = $2 & y = $3 implies y = x \/ A1.(s+1)); A1: for n being Nat for x being Subset of X ex y being Subset of X st P[n,x,y] proof let n be Nat; let x be Subset of X; take x \/ A1.(n+1); thus thesis; end; consider F being SetSequence of X such that A2: F.0 = A1.0 and A3: for n being Nat holds P[n,F.n,F.(n+1)] from RECDEF_1:sch 2(A1 ); take F; thus F.0 = A1.0 by A2; let n be Nat; reconsider n as Element of NAT by ORDINAL1:def 12; P[n,F.n,F.(n+1)] by A3; hence thesis; end; uniqueness proof let S1,S2 be SetSequence of X such that A4: S1.0 = A1.0 and A5: for n being Nat holds S1.(n+1) = S1.n \/ A1.(n+1) and A6: S2.0 = A1.0 and A7: for n being Nat holds S2.(n+1) = S2.n \/ A1.(n+1); defpred P[object] means S1.$1 = S2.$1; for n being object holds n in NAT implies P[n] proof let n be object; assume n in NAT; then reconsider n as Element of NAT; A8: for k st P[k] holds P[k+1] proof let k; assume S1.k = S2.k; hence S1.(k+1) = S2.k \/ A1.(k+1) by A5 .= S2.(k+1) by A7; end; A9: P[0] by A4,A6; for k being Nat holds P[k] from NAT_1:sch 2(A9,A8); then S1.n = S2.n; hence thesis; end; hence thesis; end; end; theorem Th8: (Partial_Intersection A1).n c= A1.n proof per cases by NAT_1:6; suppose n = 0; hence thesis by Def1; end; suppose ex k being Nat st n = k+1; then consider k such that A1: n = k+1; (Partial_Intersection A1).(k+1) = (Partial_Intersection A1).k /\ A1.(k +1) by Def1; hence thesis by A1,XBOOLE_1:17; end; end; theorem Th9: A1.n c= (Partial_Union A1).n proof per cases by NAT_1:6; suppose n = 0; hence thesis by Def2; end; suppose ex k being Nat st n = k+1; then consider k such that A1: n = k+1; (Partial_Union A1).(k+1) = (Partial_Union A1).k \/ A1.(k+1) by Def2; hence thesis by A1,XBOOLE_1:7; end; end; theorem Th10: Partial_Intersection A1 is non-ascending proof now let n be Nat; (Partial_Intersection A1).(n+1) = (Partial_Intersection A1).n /\ A1.(n +1) by Def1; hence (Partial_Intersection A1).(n+1) c= (Partial_Intersection A1).n by XBOOLE_1:17; end; hence thesis by PROB_2:6; end; theorem Th11: Partial_Union A1 is non-descending proof now let n be Nat; (Partial_Union A1).(n+1) = (Partial_Union A1).n \/ A1.(n+1) by Def2; hence (Partial_Union A1).n c= (Partial_Union A1).(n+1) by XBOOLE_1:7; end; hence thesis by PROB_2:7; end; theorem Th12: for x being object holds x in (Partial_Intersection A1).n iff for k st k <= n holds x in A1.k proof let x be object; defpred P[Nat] means (for k st k <= $1 holds x in A1.k) implies x in ( Partial_Intersection A1).$1; A1: for i st P[i] holds P[i+1] proof let i such that A2: (for k st k <= i holds x in A1.k) implies x in ( Partial_Intersection A1).i; assume for k st k <= i+1 holds x in A1.k; then A3: ( for k st k <= i holds x in A1.k)& x in A1.(i+1) by NAT_1:12; (Partial_Intersection A1).(i+1) = (Partial_Intersection A1).i /\ A1.( i+1) by Def1; hence thesis by A2,A3,XBOOLE_0:def 4; end; thus x in (Partial_Intersection A1).n implies for k st k <= n holds x in A1. k proof assume A4: x in (Partial_Intersection A1).n; for k st k <= n holds x in A1.k proof A5: Partial_Intersection A1 is non-ascending by Th10; let k such that A6: k <= n; A7: (Partial_Intersection A1).k c= A1.k by Th8; (Partial_Intersection A1).n c= (Partial_Intersection A1).k by A6,A5, PROB_1:def 4; then (Partial_Intersection A1).n c= A1.k by A7; hence thesis by A4; end; hence thesis; end; A8: P[0] proof assume for k st k <= 0 holds x in A1.k; then x in A1.0; hence thesis by Def1; end; for n holds P[n] from NAT_1:sch 2(A8,A1); hence thesis; end; theorem Th13: x in (Partial_Union A1).n iff ex k st k <= n & x in A1.k proof defpred P[Nat] means (x in (Partial_Union A1).$1 implies ex k st k <= $1 & x in A1.k); A1: for i st P[i] holds P[i+1] proof let i such that A2: x in (Partial_Union A1).i implies ex k st k <= i & x in A1.k; assume A3: x in (Partial_Union A1).(i+1); A4: (Partial_Union A1).(i+1) = (Partial_Union A1).i \/ A1.(i+1) by Def2; now per cases by A3,A4,XBOOLE_0:def 3; case x in (Partial_Union A1).i; then consider k such that A5: k <= i & x in A1.k by A2; take k; thus thesis by A5,NAT_1:12; end; case x in A1.(i+1); hence thesis; end; end; hence thesis; end; A6: P[0] proof assume A7: x in (Partial_Union A1).0; take 0; thus thesis by A7,Def2; end; for n holds P[n] from NAT_1:sch 2(A6,A1); hence x in (Partial_Union A1).n implies ex k st k <= n & x in A1.k; given i such that A8: i <= n and A9: x in A1.i; A1.i c= (Partial_Union A1).i by Th9; then A10: x in (Partial_Union A1).i by A9; A11: Partial_Union A1 is non-descending by Th11; (Partial_Union A1).i c= (Partial_Union A1).n by A8,A11,PROB_1:def 5; hence thesis by A10; end; theorem Th14: Intersection Partial_Intersection A1 = Intersection A1 proof thus Intersection Partial_Intersection A1 c= Intersection A1 proof let x be object; assume A1: x in Intersection Partial_Intersection A1; for n be Nat holds x in A1.n proof let n be Nat; x in (Partial_Intersection A1).n by A1,PROB_1:13; hence thesis by Th12; end; hence thesis by PROB_1:13; end; let x be object; assume A2: x in Intersection A1; for n be Nat holds x in (Partial_Intersection A1).n proof let n be Nat; for k st k <= n holds x in A1.k by A2,PROB_1:13; hence thesis by Th12; end; hence thesis by PROB_1:13; end; theorem Th15: Union Partial_Union A1 = Union A1 proof thus Union Partial_Union A1 c= Union A1 proof let x be object; assume x in Union Partial_Union A1; then consider n being Nat such that A1: x in (Partial_Union A1).n by PROB_1:12; consider k such that k <= n and A2: x in A1.k by A1,Th13; thus thesis by A2,PROB_1:12; end; let x be object; assume x in Union A1; then consider n being Nat such that A3: x in A1.n by PROB_1:12; x in (Partial_Union A1).n by A3,Th13; hence thesis by PROB_1:12; end; definition let X be set, A1 be SetSequence of X; func Partial_Diff_Union A1 -> SetSequence of X means :Def3: it.0 = A1.0 & for n being Nat holds it.(n+1) = A1.(n+1) \ (Partial_Union A1).n; existence proof defpred P[set,set,set] means for x,y being Subset of X,s being Nat holds (s = $1 & x = $2 & y = $3 implies y = A1.(s+1) \ (Partial_Union A1).s); set A = A1.0; A1: for n being Nat for x being Subset of X ex y being Subset of X st P[n,x,y] proof let n be Nat; let x be Subset of X; take A1.(n+1) \ (Partial_Union A1).n; thus thesis; end; consider F being SetSequence of X such that A2: F.0 = A & for n being Nat holds P[n,F.n,F.(n+1)] from RECDEF_1:sch 2(A1); for n holds F.(n+1) = A1.(n+1) \ (Partial_Union A1).n proof let n; reconsider n1 = n as Element of NAT by ORDINAL1:def 12; for x,y being Subset of X,s being Nat holds s = n1 & x = F.n1 & y = F. (n1+1) implies y = A1.(s+1) \ (Partial_Union A1).s by A2; hence thesis; end; hence thesis by A2; end; uniqueness proof let S1,S2 be SetSequence of X such that A3: S1.0 = A1.0 and A4: for n being Nat holds S1.(n+1) = A1.(n+1) \ (Partial_Union A1).n and A5: S2.0 = A1.0 and A6: for n being Nat holds S2.(n+1) = A1.(n+1) \ (Partial_Union A1).n; defpred P[object] means S1.$1 = S2.$1; for n being object holds n in NAT implies P[n] proof let n be object; assume n in NAT; then reconsider n as Element of NAT; A7: for k st P[k] holds P[k+1] proof let k; assume S1.k = S2.k; thus S1.(k+1) = A1.(k+1) \ (Partial_Union A1).k by A4 .= S2.(k+1) by A6; end; A8: P[0] by A3,A5; for k being Nat holds P[k] from NAT_1:sch 2(A8,A7); then S1.n = S2.n; hence thesis; end; hence thesis; end; end; theorem Th16: x in (Partial_Diff_Union A1).n iff x in A1.n & for k st k < n holds not x in A1.k proof thus x in (Partial_Diff_Union A1).n implies x in A1.n & for k st k < n holds not x in A1.k proof assume A1: x in (Partial_Diff_Union A1).n; now per cases by NAT_1:6; case n = 0; hence thesis by A1,Def3; end; case ex n1 being Nat st n = n1 + 1; then consider n1 being Nat such that A2: n = n1+1; A3: x in A1.(n1+1) \ (Partial_Union A1).n1 by A1,A2,Def3; then A4: not x in (Partial_Union A1).n1 by XBOOLE_0:def 5; for k st k < n holds not x in A1.k proof let k; assume k < n; then k <= n1 by A2,NAT_1:13; hence thesis by A4,Th13; end; hence thesis by A2,A3,XBOOLE_0:def 5; end; end; hence thesis; end; assume that A5: x in A1.n and A6: for k st k < n holds not x in A1.k; now per cases by NAT_1:6; case n = 0; hence thesis by A5,Def3; end; case ex n1 being Nat st n = n1 + 1; then consider n1 being Nat such that A7: n = n1+1; for k st k <= n1 holds not x in A1.k proof let k; assume k <= n1; then k < n1+1 by NAT_1:13; hence thesis by A6,A7; end; then not x in (Partial_Union A1).n1 by Th13; then x in A1.(n1+1) \ (Partial_Union A1).n1 by A5,A7,XBOOLE_0:def 5; hence thesis by A7,Def3; end; end; hence thesis; end; theorem Th17: (Partial_Diff_Union A1).n c= A1.n by Th16; theorem Th18: (Partial_Diff_Union A1).n c= (Partial_Union A1).n proof (Partial_Diff_Union A1).n c= A1.n & A1.n c= (Partial_Union A1).n by Th9,Th17; hence thesis; end; theorem Th19: Partial_Union (Partial_Diff_Union A1) = Partial_Union A1 proof for n being Nat holds (Partial_Union (Partial_Diff_Union A1)) .n = (Partial_Union A1).n proof set A2 = Partial_Diff_Union A1; defpred P[set] means (Partial_Union A2).$1 = (Partial_Union A1).$1; A1: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that A2: (Partial_Union A2).k = (Partial_Union A1).k; thus (Partial_Union A2).(k+1) = A2.(k+1) \/ (Partial_Union A2).k by Def2 .= (A1.(k+1) \ (Partial_Union A1).k) \/ (Partial_Union A1).k by A2,Def3 .= A1.(k+1) \/ (Partial_Union A1).k by XBOOLE_1:39 .= (Partial_Union A1).(k+1) by Def2; end; (Partial_Union (Partial_Diff_Union A1)).0 = A2.0 by Def2 .= A1.0 by Def3 .= (Partial_Union A1).0 by Def2; then A3: P[0]; thus for k being Nat holds P[k] from NAT_1:sch 2(A3,A1 ); end; hence thesis; end; theorem Th20: Union Partial_Diff_Union A1 = Union A1 proof thus Union Partial_Diff_Union A1 = Union Partial_Union (Partial_Diff_Union A1) by Th15 .= Union Partial_Union A1 by Th19 .= Union A1 by Th15; end; definition let X,A1; redefine attr A1 is disjoint_valued means for m,n st m <> n holds A1. m misses A1.n; compatibility proof thus A1 is disjoint_valued implies for m,n st m <> n holds A1.m misses A1. n by PROB_2:def 2; assume A1: for m,n st m <> n holds A1.m misses A1.n; now let x,y be object; assume A2: x <> y; per cases; suppose x in dom A1 & y in dom A1; hence A1.x misses A1.y by A1,A2; end; suppose not (x in dom A1 & y in dom A1); then A1.x = {} or A1.y = {} by FUNCT_1:def 2; hence A1.x misses A1.y; end; end; hence thesis by PROB_2:def 2; end; end; registration let X,A1; cluster Partial_Diff_Union A1 -> disjoint_valued; coherence proof for m,n st m <> n holds (Partial_Diff_Union A1).n misses ( Partial_Diff_Union A1).m proof let m,n such that A1: m <> n; assume (Partial_Diff_Union A1).n meets (Partial_Diff_Union A1).m; then consider x being object such that A2: x in (Partial_Diff_Union A1).n and A3: x in (Partial_Diff_Union A1).m by XBOOLE_0:3; per cases by A1,XXREAL_0:1; suppose m < n; then not x in A1.m by A2,Th16; hence contradiction by A3,Th16; end; suppose n < m; then not x in A1.n by A3,Th16; hence contradiction by A2,Th16; end; end; hence thesis; end; end; registration let X be set, Si be SigmaField of X, XSeq be SetSequence of Si; cluster Partial_Intersection XSeq -> Si-valued; coherence proof defpred P[set] means (Partial_Intersection XSeq).$1 in Si; A1: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A2: (Partial_Intersection XSeq).k in Si; (Partial_Intersection XSeq).k /\ XSeq.(k+1) is Event of Si by A2, PROB_1:19; then (Partial_Intersection XSeq).k /\ XSeq.(k+1) in Si; hence thesis by Def1; end; XSeq.0 in rng XSeq & (Partial_Intersection XSeq).0 = XSeq.0 by Def1, NAT_1:51; then A3: P[0]; for k being Nat holds P[k] from NAT_1:sch 2(A3,A1); then rng Partial_Intersection XSeq c= Si by NAT_1:52; hence thesis; end; end; registration let X be set, Si be SigmaField of X, XSeq be SetSequence of Si; cluster Partial_Union XSeq -> Si-valued; coherence proof defpred P[set] means (Partial_Union XSeq).$1 in Si; A1: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A2: (Partial_Union XSeq).k in Si; (Partial_Union XSeq).k \/ XSeq.(k+1) is Event of Si by A2,PROB_1:21; then (Partial_Union XSeq).k \/ XSeq.(k+1) in Si; hence thesis by Def2; end; XSeq.0 in rng XSeq & (Partial_Union XSeq).0 = XSeq.0 by Def2,NAT_1:51; then A3: P[0]; for k being Nat holds P[k] from NAT_1:sch 2(A3,A1); then rng Partial_Union XSeq c= Si by NAT_1:52; hence thesis; end; end; registration let X be set, Si be SigmaField of X, XSeq be SetSequence of Si; cluster Partial_Diff_Union XSeq -> Si-valued; coherence proof A1: XSeq.0 in rng XSeq & (Partial_Diff_Union XSeq).0 = XSeq.0 by Def3,NAT_1:51; for m being Nat holds (Partial_Diff_Union XSeq).m in Si proof let m be Nat; now per cases by NAT_1:6; case m = 0; hence thesis by A1; end; case ex k being Nat st m = k+1; then consider k being Nat such that A2: m = k+1; reconsider k as Element of NAT by ORDINAL1:def 12; XSeq.(k+1) \ (Partial_Union XSeq).k in Si; hence thesis by A2,Def3; end; end; hence thesis; end; then rng Partial_Diff_Union XSeq c= Si by NAT_1:52; hence thesis; end; end; theorem YSeq = Partial_Intersection XSeq implies YSeq.0 = XSeq.0 & for n holds YSeq.(n+1) = YSeq.n /\ XSeq.(n+1) by Def1; theorem YSeq = Partial_Union XSeq implies YSeq.0 = XSeq.0 & for n holds YSeq. (n+1) = YSeq.n \/ XSeq.(n+1) by Def2; theorem (Partial_Intersection XSeq).n c= XSeq.n by Th8; theorem XSeq.n c= (Partial_Union XSeq).n by Th9; theorem for x being object holds x in (Partial_Intersection XSeq).n iff for k st k <= n holds x in XSeq.k proof reconsider XSeq as SetSequence of X; let x be object; x in (Partial_Intersection XSeq).n iff for k st k <= n holds x in XSeq.k by Th12; hence thesis; end; theorem x in (Partial_Union XSeq).n iff ex k st k <= n & x in XSeq.k proof reconsider XSeq as SetSequence of X; x in (Partial_Union XSeq).n iff ex k st k <= n & x in XSeq.k by Th13; hence thesis; end; theorem Partial_Intersection XSeq is non-ascending by Th10; theorem Partial_Union XSeq is non-descending by Th11; theorem Intersection Partial_Intersection XSeq = Intersection XSeq by Th14; theorem Union Partial_Union XSeq = Union XSeq by Th15; theorem YSeq = Partial_Diff_Union XSeq implies YSeq.0 = XSeq.0 & for n holds YSeq.(n+1) = XSeq.(n+1) \ (Partial_Union XSeq).n by Def3; theorem x in (Partial_Diff_Union XSeq).n iff x in XSeq.n & for k st k < n holds not x in XSeq.k proof reconsider XSeq as SetSequence of X; x in (Partial_Diff_Union XSeq).n iff x in XSeq.n & for k st k < n holds not x in XSeq.k by Th16; hence thesis; end; theorem (Partial_Diff_Union XSeq).n c= XSeq.n by Th17; theorem (Partial_Diff_Union XSeq).n c= (Partial_Union XSeq).n by Th18; theorem Partial_Union (Partial_Diff_Union XSeq) = Partial_Union XSeq by Th19; theorem Union Partial_Diff_Union XSeq = Union XSeq by Th20; theorem Th37: (P * Partial_Union ASeq) is non-decreasing proof Partial_Union ASeq is non-descending by Th11; hence thesis by Th6; end; theorem (P * Partial_Intersection ASeq) is non-increasing proof Partial_Intersection ASeq is non-ascending by Th10; hence thesis by Th7; end; theorem Partial_Sums(P * ASeq) is non-decreasing proof for n being Nat holds (P * ASeq).n >= 0 by Th4; hence thesis by SERIES_1:16; end; theorem Th40: (P * Partial_Union ASeq).0 = Partial_Sums(P * ASeq).0 proof A1: dom (P * ASeq) = NAT by SEQ_1:1; dom (P * Partial_Union ASeq) = NAT by SEQ_1:1; then A2: (P * Partial_Union ASeq).0 = P.((Partial_Union ASeq).0) by FUNCT_1:12 .= P.(ASeq.0) by Def2; Partial_Sums(P * ASeq).0 = (P * ASeq).0 by SERIES_1:def 1 .= P.(ASeq.0) by A1,FUNCT_1:12; hence thesis by A2; end; theorem Th41: P * Partial_Union ASeq is convergent & lim (P * Partial_Union ASeq) = upper_bound (P * Partial_Union ASeq) & lim (P * Partial_Union ASeq) = P.Union ASeq proof A1: P * Partial_Union ASeq is non-decreasing by Th37; A2: Partial_Union ASeq is non-descending by Th11; then P * Partial_Union ASeq is convergent by PROB_2:10; then A3: P * Partial_Union ASeq is bounded; lim (P * Partial_Union ASeq) = P.Union (Partial_Union ASeq) by A2,PROB_2:10 .= P.Union ASeq by Th15; hence thesis by A2,A3,A1,PROB_2:10,RINFSUP1:24; end; theorem Th42: ASeq is disjoint_valued implies for n,m st n < m holds ( Partial_Union ASeq).n misses ASeq.m proof assume A1: ASeq is disjoint_valued; let n,m such that A2: n < m; assume (Partial_Union ASeq).n meets ASeq.m; then consider x being object such that A3: x in (Partial_Union ASeq).n and A4: x in ASeq.m by XBOOLE_0:3; reconsider ASeq as SetSequence of Omega; consider k being Nat such that A5: k <= n and A6: x in ASeq.k by A3,Th13; ASeq.k misses ASeq.m by A1,A2,A5; then ASeq.k /\ ASeq.m = {}; hence contradiction by A4,A6,XBOOLE_0:def 4; end; theorem Th43: ASeq is disjoint_valued implies (P * Partial_Union ASeq).n = Partial_Sums(P * ASeq).n proof A1: dom (P * ASeq) = NAT by SEQ_1:1; defpred P[Nat] means (P * Partial_Union ASeq).$1 = Partial_Sums(P * ASeq). $1; A2: dom (P * Partial_Union ASeq) = NAT by SEQ_1:1; assume A3: ASeq is disjoint_valued; A4: for k st P[k] holds P[k+1] proof let k such that A5: (P * Partial_Union ASeq).k = Partial_Sums(P * ASeq).k; k < k+1 by NAT_1:13; then A6: (Partial_Union ASeq).k misses ASeq.(k+1) by A3,Th42; reconsider k as Element of NAT by ORDINAL1:def 12; A7: Partial_Sums(P * ASeq).(k+1) =Partial_Sums(P * ASeq).k + (P * ASeq).( k+1) by SERIES_1:def 1 .=Partial_Sums(P * ASeq).k + P.(ASeq.(k+1)) by A1,FUNCT_1:12; (P * Partial_Union ASeq).(k+1) = P.((Partial_Union ASeq).(k+1)) by A2, FUNCT_1:12 .= P.((Partial_Union ASeq).k \/ ASeq.(k+1)) by Def2 .= P.((Partial_Union ASeq).k) + P.(ASeq.(k+1)) by A6,PROB_1:def 8 .= (P * Partial_Union ASeq).k + P.(ASeq.(k+1)) by A2,FUNCT_1:12; hence thesis by A5,A7; end; A8: P[0] by Th40; for k holds P[k] from NAT_1:sch 2(A8,A4); hence thesis; end; theorem Th44: ASeq is disjoint_valued implies (P * Partial_Union ASeq) = Partial_Sums(P * ASeq) by Th43; theorem Th45: ASeq is disjoint_valued implies Partial_Sums(P * ASeq) is convergent & lim Partial_Sums(P * ASeq) = upper_bound Partial_Sums(P * ASeq) & lim Partial_Sums(P * ASeq) = P.Union ASeq proof assume ASeq is disjoint_valued; then (P * Partial_Union ASeq) = Partial_Sums(P * ASeq) by Th44; hence thesis by Th41; end; theorem Th46: ASeq is disjoint_valued implies P.(Union ASeq) = Sum(P * ASeq) proof assume ASeq is disjoint_valued; then lim Partial_Sums(P * ASeq) = P.Union ASeq by Th45; hence thesis by SERIES_1:def 3; end; definition let X,F1,n; redefine func F1.n -> Subset of X; coherence proof per cases; suppose n in dom F1; hence thesis by FINSEQ_2:11; end; suppose not n in dom F1; then F1.n = {} by FUNCT_1:def 2; hence thesis by SUBSET_1:1; end; end; end; theorem ex F1 being FinSequence of bool X st for k st k in dom F1 holds F1.k = X proof now let n be Element of NAT; set F1 = n |-> X; A1: dom F1 = Seg n by FUNCOP_1:13; rng F1 c= bool X proof let x be object; assume x in rng F1; then ex i be Nat st i in dom F1 & F1.i = x by FINSEQ_2:10; then x = X by A1,FINSEQ_2:57; hence thesis by ZFMISC_1:def 1; end; then A2: F1 is FinSequence of bool X by FINSEQ_1:def 4; for k being Nat st k in dom F1 holds F1.k = X by A1,FINSEQ_2:57; hence thesis by A2; end; hence thesis; end; theorem for F1 being FinSequence of bool X holds union rng F1 is Subset of X; definition let X be set, F1 be FinSequence of bool X; redefine func Union F1 -> Subset of X; coherence proof Union F1 = union rng F1 by CARD_3:def 4; hence thesis; end; end; theorem Th49: x in Union F1 iff ex k st k in dom F1 & x in F1.k proof set Y = union rng F1; A1: for x holds x in Y iff ex k st k in dom F1 & x in F1.k proof let x; thus x in Y implies ex k st k in dom F1 & x in F1.k proof assume x in Y; then consider Z such that A2: x in Z and A3: Z in rng F1 by TARSKI:def 4; ex i being Nat st i in dom F1 & Z = F1.i by A3,FINSEQ_2:10; hence thesis by A2; end; thus (ex k st k in dom F1 & x in F1.k) implies x in Y proof given i such that A4: i in dom F1 and A5: x in F1.i; F1.i in rng F1 by A4,FUNCT_1:def 3; hence thesis by A5,TARSKI:def 4; end; end; Y = Union F1 by CARD_3:def 4; hence thesis by A1; end; definition let X, F1; func Complement F1 -> FinSequence of bool X means :Def5: len it = len F1 & for n st n in dom it holds it.n = (F1.n)`; existence proof deffunc F(Nat) = (F1.$1)`; consider f being FinSequence of bool X such that A1: len f = len F1 & for n being Nat st n in dom f holds f.n = F(n) from FINSEQ_2:sch 1; take f; thus thesis by A1; end; uniqueness proof let F2,F3 be FinSequence of bool X such that A2: len F2 = len F1 and A3: for n st n in dom F2 holds F2.n = (F1.n)` and A4: len F3 = len F1 and A5: for n st n in dom F3 holds F3.n = (F1.n)`; dom F2 = dom F3 & for k being Nat st k in dom F2 holds F2.k = F3.k proof thus A6: dom F2 = Seg len F3 by A2,A4,FINSEQ_1:def 3 .= dom F3 by FINSEQ_1:def 3; let k be Nat; assume A7: k in dom F2; hence F2.k = (F1.k)` by A3 .= F3.k by A5,A6,A7; end; hence thesis by FINSEQ_1:13; end; end; definition let X, F1; func Intersection F1 -> Subset of X equals :Def6: (Union Complement F1)` if F1 <> {} otherwise {}; coherence by SUBSET_1:1; consistency; end; theorem Th50: dom Complement F1 = dom F1 proof thus dom Complement F1 = Seg len Complement F1 by FINSEQ_1:def 3 .= Seg len F1 by Def5 .= dom F1 by FINSEQ_1:def 3; end; theorem Th51: for x being object holds F1 <> {} implies (x in Intersection F1 iff for k st k in dom F1 holds x in F1.k ) proof let x be object; A1: for n st n in dom F1 holds X \ (Complement F1).n = F1.n proof let n; assume n in dom F1; then A2: n in dom Complement F1 by Th50; X \ (Complement F1).n = ((Complement F1).n)` by SUBSET_1:def 4 .= ((F1.n)`)` by A2,Def5 .= F1.n; hence thesis; end; assume A3: F1 <> {}; then A4: dom F1 <> {} by RELAT_1:41; A5: x in X & (for n st n in dom F1 holds not x in (Complement F1).n) iff for n st n in dom F1 holds x in F1.n proof hereby assume that A6: x in X and A7: for n st n in dom F1 holds not x in (Complement F1).n; let n such that A8: n in dom F1; not x in (Complement F1).n by A7,A8; then x in X \ (Complement F1).n by A6,XBOOLE_0:def 5; hence x in F1.n by A1,A8; end; assume A9: for n st n in dom F1 holds x in F1.n; A10: now let n be Element of NAT such that A11: n in dom F1; x in F1.n by A9,A11; then x in X \ (Complement F1).n by A1,A11; hence x in X & not x in (Complement F1).n by XBOOLE_0:def 5; end; ex a being object st a in dom F1 by A4,XBOOLE_0:def 1; hence thesis by A10; end; dom Complement F1 = dom F1 by Th50; then A12: x in X & (not x in Union (Complement F1)) iff x in X & for n st n in dom F1 holds not x in (Complement F1).n by Th49; x in (Union Complement F1)` iff x in X \ Union Complement F1 by SUBSET_1:def 4; hence thesis by A3,A12,A5,Def6,XBOOLE_0:def 5; end; theorem Th52: F1 <> {} implies (x in meet rng F1 iff for n st n in dom F1 holds x in F1.n) proof assume F1 <> {}; then A1: rng F1 <> {} by RELAT_1:41; A2: now let x; assume A3: for n st n in dom F1 holds x in F1.n; now let Y; assume Y in rng F1; then consider n be object such that A4: n in dom F1 and A5: Y = F1.n by FUNCT_1:def 3; thus x in Y by A3,A4,A5; end; hence x in meet rng F1 by A1,SETFAM_1:def 1; end; now let x; assume A6: x in meet rng F1; now let k; assume k in dom F1; then F1.k in rng F1 by FUNCT_1:3; hence x in F1.k by A6,SETFAM_1:def 1; end; hence for n st n in dom F1 holds x in F1.n; end; hence thesis by A2; end; theorem Intersection F1 = meet rng F1 proof per cases; suppose A1: F1 <> {}; now let x be object; x in Intersection F1 iff for n st n in dom F1 holds x in F1.n by A1,Th51; hence x in Intersection F1 iff x in meet rng F1 by A1,Th52; end; hence thesis by TARSKI:2; end; suppose F1 = {}; hence thesis by Def6,RELAT_1:38,SETFAM_1:1; end; end; theorem Th54: for F1 being FinSequence of bool X holds ex A1 being SetSequence of X st (for k st k in dom F1 holds A1.k = F1.k) & for k st not k in dom F1 holds A1.k = {} proof deffunc G(object) = {}; let F1 be FinSequence of bool X; defpred P[object] means $1 in dom F1; deffunc F(object) = F1.$1; ex f being Function st dom f = NAT & for k being object st k in NAT holds ( P[k] implies f.k=F(k)) & (not P[k] implies f.k=G(k)) from PARTFUN1:sch 1; then consider f being Function such that A1: dom f = NAT and A2: for x being object st x in NAT holds (x in dom F1 implies f.x = F1.x) & (not x in dom F1 implies f.x = {}); A3: for x st x in dom F1 holds F1.x in bool X proof let x; assume x in dom F1; then F1.x in rng F1 by FUNCT_1:3; hence thesis; end; for x st x in NAT holds f.x in bool X proof let x; assume A4: x in NAT; per cases; suppose not x in dom F1; then f.x = {} by A2,A4; then f.x c= X; hence thesis; end; suppose A5: x in dom F1; then f.x = F1.x by A2; hence thesis by A3,A5; end; end; then reconsider f as SetSequence of X by A1,FUNCT_2:3; take f; thus for k st k in dom F1 holds f.k = F1.k by A2; let k; k in NAT by ORDINAL1:def 12; hence thesis by A2; end; theorem Th55: for F1 being FinSequence of bool X for A1 being SetSequence of X st (for k st k in dom F1 holds A1.k = F1.k) & (for k st not k in dom F1 holds A1.k = {}) holds A1.0={} & Union A1 = Union F1 proof let F1 be FinSequence of bool X; let A1 be SetSequence of X such that A1: for k st k in dom F1 holds A1.k = F1.k and A2: for k st not k in dom F1 holds A1.k = {}; thus A1.0 = {} by A2,Th1; thus Union A1 = Union F1 proof thus Union A1 c= Union F1 proof let x be object; assume x in Union A1; then consider n being Nat such that A3: x in A1.n by PROB_1:12; n in dom F1 & x in F1.n by A1,A2,A3; hence thesis by Th49; end; let x be object; assume x in Union F1; then consider n such that A4: n in dom F1 & x in F1.n by Th49; n in NAT & x in A1.n by A1,A4; hence thesis by PROB_1:12; end; end; definition :: czy wystarczy rejestracja? let X be set, Si be SigmaField of X; redefine mode FinSequence of Si -> FinSequence of bool X; coherence proof let f be FinSequence of Si; thus rng f c= bool X by XBOOLE_1:1; end; end; definition let X be set, Si be SigmaField of X, FSi be FinSequence of Si,n; redefine func FSi.n -> Event of Si; coherence proof per cases; suppose n in dom FSi; hence thesis by FINSEQ_2:11; end; suppose not n in dom FSi; then FSi.n = {} by FUNCT_1:def 2; hence thesis by PROB_1:22; end; end; end; theorem Th56: for FSi being FinSequence of Si holds ex ASeq being SetSequence of Si st (for k st k in dom FSi holds ASeq.k = FSi.k) & for k st not k in dom FSi holds ASeq.k = {} proof let FSi be FinSequence of Si; consider A1 being SetSequence of X such that A1: for k st k in dom FSi holds A1.k = FSi.k and A2: for k st not k in dom FSi holds A1.k = {} by Th54; for n being Nat holds A1.n in Si proof let n be Nat; per cases; suppose not n in dom FSi; then A1.n = {} by A2; hence thesis by PROB_1:4; end; suppose n in dom FSi; then A1.n = FSi.n by A1; hence thesis; end; end; then rng A1 c= Si by NAT_1:52; then reconsider A1 as SetSequence of Si by RELAT_1:def 19; take A1; thus thesis by A1,A2; end; theorem Th57: for FSi being FinSequence of Si holds Union FSi in Si proof let FSi be FinSequence of Si; consider ASeq being SetSequence of Si such that A1: ( for k st k in dom FSi holds ASeq.k = FSi.k)& for k st not k in dom FSi holds ASeq.k = {} by Th56; reconsider ASeq as SetSequence of X; ( for k st k in dom FSi holds ASeq.k = FSi.k)& for k st not k in dom FSi holds ASeq.k = {} by A1; then Union ASeq = Union FSi by Th55; hence thesis by PROB_1:17; end; registration let X be set, S be SigmaField of X, F being FinSequence of S; cluster Complement F -> S-valued; coherence proof set G = Complement F; let x be object; assume x in rng G; then consider y being object such that A1: y in dom G and A2: x = G.y by FUNCT_1:def 3; reconsider y as Nat by A1; G.y = (F.y)` by A1,Def5; then G.y is Event of S by PROB_1:20; hence x in S by A2; end; end; theorem for FSi being FinSequence of Si holds Intersection FSi in Si proof let FSi be FinSequence of Si; per cases; suppose FSi = {}; then Intersection FSi = {} by Def6; hence thesis by PROB_1:4; end; suppose A1: FSi <> {}; rng Complement FSi c= Si; then reconsider C = Complement FSi as FinSequence of Si by FINSEQ_1:def 4; A2: Union C in Si by Th57; Intersection FSi = (Union Complement FSi)` by A1,Def6; hence thesis by A2,PROB_1:def 1; end; end; reserve FSeq for FinSequence of Sigma; theorem Th59: dom(P * FSeq) = dom FSeq proof for x being object holds x in dom (P * FSeq) iff x in dom FSeq proof let x be object; thus x in dom (P * FSeq) implies x in dom FSeq by FUNCT_1:11; assume A1: x in dom FSeq; then reconsider k=x as Element of NAT; FSeq.k in Sigma; then FSeq.k in dom P by FUNCT_2:def 1; hence thesis by A1,FUNCT_1:11; end; hence thesis by TARSKI:2; end; theorem Th60: P * FSeq is FinSequence of REAL proof dom (P * FSeq) = dom FSeq by Th59; then ex n being Nat st dom (P * FSeq) = Seg n by FINSEQ_1:def 2; then reconsider RSeq = P * FSeq as FinSequence by FINSEQ_1:def 2; rng (P * FSeq) c= REAL; then rng RSeq c= REAL; hence thesis by FINSEQ_1:def 4; end; definition let Omega,Sigma,FSeq,P; redefine func P * FSeq -> FinSequence of REAL; coherence by Th60; end; theorem Th61: len (P * FSeq) = len FSeq proof dom(P * FSeq) = dom FSeq by Th59; then Seg len (P * FSeq) = dom FSeq by FINSEQ_1:def 3; hence thesis by FINSEQ_1:def 3; end; theorem Th62: len RFin = 0 implies Sum RFin = 0 proof assume A1: len RFin=0; 0 in REAL by XREAL_0:def 1; then A2: addreal is having_a_unity by RVSUM_1:1,SETWISEO:def 2; thus Sum(RFin) = addreal $$ RFin by RVSUM_1:def 12 .= 0 by A1,A2,BINOP_2:2,FINSOP_1:def 1; end; theorem Th63: len RFin >= 1 implies ex f being Real_Sequence st f.1 = RFin.1 & (for n st 0 <> n & n < len RFin holds f.(n+1) = f.n+RFin.(n+1)) & Sum(RFin) = f .(len RFin) proof assume len RFin >= 1; then consider f be sequence of REAL such that A1: f.1 = RFin.1 and A2: for n being Nat st 0 <> n & n < len RFin holds f.(n+1) = addreal.(f.n,RFin.(n+1)) and A3: addreal "**" RFin = f.(len RFin) by FINSOP_1:1; take f; for n st 0 <> n & n < len RFin holds f.(n+1) = f.n+ RFin.(n+1) proof let n; reconsider n1=n as Element of NAT by ORDINAL1:def 12; assume that A4: 0 <> n and A5: n < len RFin; thus f.(n+1) = addreal.(f.n1,RFin.(n1+1)) by A2,A4,A5 .= f.n+ RFin.(n+1) by BINOP_2:def 9; end; hence thesis by A1,A3,RVSUM_1:def 12; end; theorem Th64: for FSeq being FinSequence of Sigma, ASeq being SetSequence of Sigma st (for k st k in dom FSeq holds ASeq.k = FSeq.k) & (for k st not k in dom FSeq holds ASeq.k = {}) holds Partial_Sums(P * ASeq) is convergent & Sum(P * ASeq) = Partial_Sums(P * ASeq).(len FSeq) & P.(Union ASeq) <= Sum(P * ASeq) & Sum(P * FSeq) = Sum(P * ASeq) proof let FSeq be FinSequence of Sigma, ASeq be SetSequence of Sigma such that A1: for k st k in dom FSeq holds ASeq.k = FSeq.k and A2: for k st not k in dom FSeq holds ASeq.k = {}; reconsider XSeq = ASeq as SetSequence of Omega; (for k st k in dom FSeq holds XSeq.k = FSeq.k) & for k st not k in dom FSeq holds XSeq.k = {} by A1,A2; then A3: ASeq.0 ={} by Th55; A4: (P * ASeq).0 = P.(ASeq.0) by FUNCT_2:15 .= 0 by A3,VALUED_0:def 19; A5: for k st k in dom FSeq holds (P * ASeq).k = (P * FSeq).k proof let k such that A6: k in dom FSeq; k in NAT by ORDINAL1:def 12; hence (P * ASeq).k = P.(ASeq.k) by FUNCT_2:15 .= P.(FSeq.k) by A1,A6 .= (P * FSeq).k by A6,FUNCT_1:13; end; 1 = 0+1; then A7: Partial_Sums(P * ASeq).1 = Partial_Sums(P * ASeq).0 + (P*ASeq).1 by SERIES_1:def 1 .= (P*ASeq).0 + (P*ASeq).1 by SERIES_1:def 1 .= (P * ASeq).1 by A4; A8: len FSeq >= 1 implies Partial_Sums(P * ASeq).1=(P * FSeq).1 & for m st m <> 0 & m < len FSeq holds Partial_Sums(P*ASeq).(m+1)=Partial_Sums(P*ASeq).m+( P*FSeq).(m+1) proof assume len FSeq >= 1; then 1 in dom FSeq by Th2; hence Partial_Sums(P * ASeq).1 = (P * FSeq).1 by A5,A7; thus for m st m <> 0 & m < len FSeq holds Partial_Sums(P*ASeq).(m+1)= Partial_Sums(P*ASeq).m+(P*FSeq).(m+1) proof let m; assume that m <> 0 and A9: m < len FSeq; reconsider m1 = m as Element of NAT by ORDINAL1:def 12; m+1 in Seg len FSeq by A9,FINSEQ_3:11; then A10: m+1 in dom FSeq by FINSEQ_1:def 3; thus Partial_Sums(P*ASeq).(m+1) = Partial_Sums(P*ASeq).m1+(P*ASeq).(m1+1 ) by SERIES_1:def 1 .= Partial_Sums(P*ASeq).m+(P*FSeq).(m+1) by A5,A10; end; end; defpred P[Nat] means Partial_Sums(P * ASeq).((len FSeq + 1) + $1) = Partial_Sums(P * ASeq).(len FSeq); A11: for m being Nat holds (P * ASeq).((len FSeq + 1) + m)=0 proof set k=len FSeq + 1; let m be Nat; reconsider m1=m as Element of NAT by ORDINAL1:def 12; k + m >= k by NAT_1:11; then len FSeq + 1 + m > len FSeq by Lm1; then not len FSeq + 1 + m in dom FSeq by FINSEQ_3:25; then A12: ASeq.((len FSeq + 1) + m) = {} by A2; thus (P * ASeq).((len FSeq + 1) + m) = P.(ASeq.((len FSeq + 1) + m1)) by FUNCT_2:15 .= 0 by A12,VALUED_0:def 19; end; A13: for k st P[k] holds P[k+1] proof let k such that A14: Partial_Sums(P * ASeq).((len FSeq + 1) + k) = Partial_Sums(P * ASeq).(len FSeq); reconsider k1 = k as Element of NAT by ORDINAL1:def 12; Partial_Sums(P * ASeq).((len FSeq + 1 + k)+1) = Partial_Sums(P * ASeq ).(len FSeq + 1 + k1) + (P * ASeq).((len FSeq + 1) + (k1+1)) by SERIES_1:def 1 .= Partial_Sums(P * ASeq).(len FSeq + 1 + k) + 0 by A11; hence thesis by A14; end; now let n be Nat; (Partial_Diff_Union ASeq).n c= ASeq.n by Th17; hence (P * Partial_Diff_Union ASeq).n <= (P * ASeq).n by Th5; end; then A15: for n being Nat holds (Partial_Sums(P * Partial_Diff_Union ASeq)).n <= (Partial_Sums(P * ASeq)).n by SERIES_1:14; A16: Partial_Sums(P * Partial_Diff_Union ASeq) is convergent by Th45; Partial_Sums(P * ASeq).((len FSeq + 1) + 0) = Partial_Sums(P * ASeq).( len FSeq) + (P * ASeq).((len FSeq + 1) + 0) by SERIES_1:def 1 .= Partial_Sums(P * ASeq).(len FSeq) + 0 by A11; then A17: P[0]; A18: for k holds P[k] from NAT_1:sch 2(A17,A13); A19: for m st len FSeq + 1 <= m holds Partial_Sums(P * ASeq).m = Partial_Sums(P * ASeq).(len FSeq) proof let m; assume len FSeq + 1 <= m; then ex k being Nat st m = (len FSeq + 1) + k by NAT_1:10; hence thesis by A18; end; then A20: lim Partial_Sums(P * ASeq) = Partial_Sums(P * ASeq).(len FSeq) by Th3; then A21: Sum(P * ASeq) = Partial_Sums(P * ASeq).(len FSeq) by SERIES_1:def 3; A22: Sum(P * FSeq) = Sum(P * ASeq) proof now per cases; suppose len FSeq = 0; then len (P * FSeq) = 0 & Sum(P * ASeq) = 0 by A4,A21,Th61, SERIES_1:def 1; hence thesis by Th62; end; suppose A23: len FSeq <> 0; then 1 <= len FSeq by NAT_1:14; then A24: 1 <= len (P * FSeq) by Th61; then consider seq1 being Real_Sequence such that A25: seq1.1 = (P * FSeq).1 and A26: for n st 0 <> n & n < len (P * FSeq) holds seq1.(n+1) = seq1. n+(P * FSeq).(n+1) and A27: Sum(P * FSeq) = seq1.(len (P * FSeq)) by Th63; defpred P[object,object] means ex n st (n=$1 & (n = 0 implies $2=0) & (n <> 0 & n <= len (P * FSeq) implies $2=seq1.n) & (n <> 0 & n > len (P * FSeq) implies $2=Partial_Sums(P*ASeq).(len(P * FSeq)))); ex seq being Real_Sequence st for n holds (n=0 implies seq.n=0) & (n<>0 & n <= len (P * FSeq) implies seq.n=seq1.n) & (n<>0 & n > len (P * FSeq) implies seq.n=Partial_Sums(P*ASeq).(len (P * FSeq))) proof A28: for x being object st x in NAT ex y being object st P[x,y] proof let x be object; assume x in NAT; then reconsider n=x as Element of NAT; now per cases; case n=0; hence P[x,0]; end; case n <> 0 & n <= len (P * FSeq); hence P[x,(seq1.n)]; end; case n <> 0 & not n <= len (P * FSeq); hence P[x,Partial_Sums(P*ASeq).(len(P * FSeq))]; end; end; hence thesis; end; consider f being Function such that A29: dom f=NAT & for x being object st x in NAT holds P[x,f.x] from CLASSES1: sch 1(A28); now let x; assume x in NAT; then ex n st n=x & (n = 0 implies f.x=0) & (n <> 0 & n <= len (P * FSeq) implies f.x=seq1.n) & (n <> 0 & n > len (P * FSeq) implies f.x= Partial_Sums(P*ASeq).(len(P * FSeq))) by A29; hence f.x is real; end; then reconsider f as Real_Sequence by A29,SEQ_1:1; take seq=f; let n; n in NAT by ORDINAL1:def 12; then ex k st k=n & (k=0 implies seq.n=0) & (k<>0 & k <= len (P * FSeq) implies seq.n=seq1.k) & (k<>0 & k > len (P * FSeq) implies seq.n= Partial_Sums(P*ASeq).(len (P * FSeq))) by A29; hence thesis; end; then consider seq2 being Real_Sequence such that A30: for n holds (n=0 implies seq2.n=0) & (n<>0 & n <= len (P * FSeq) implies seq2.n=seq1.n) & (n<>0 & n > len (P * FSeq) implies seq2.n= Partial_Sums(P*ASeq).(len (P * FSeq))); defpred P[Nat] means seq2.$1 = Partial_Sums(P * ASeq).$1; A31: for k st P[k] holds P[k+1] proof let k such that A32: P[k]; now per cases; case k = 0; thus seq2.1 = Partial_Sums(P * ASeq).1 by A8,A23,A24,A25,A30, NAT_1:14; end; case A33: k <> 0 & k <= len (P * FSeq) -1; then A34: k + 0 < (len (P * FSeq) - 1) + 1 by XREAL_1:8; then A35: k < len FSeq by Th61; k+1 <= len (P * FSeq) -1 +1 by A33,XREAL_1:7; hence seq2.(k+1) = seq1.(k+1) by A30 .= seq1.k + (P * FSeq).(k+1) by A26,A33,A34 .= Partial_Sums(P * ASeq).k + (P * FSeq).(k+1) by A30,A32,A33 ,A34 .= Partial_Sums(P * ASeq).(k+1) by A8,A33,A35,NAT_1:14; end; case k <> 0 & not k <= len (P * FSeq) - 1; then A36: k+1 > len (P * FSeq) - 1 + 1 by XREAL_1:8; then k+1 >= len (P * FSeq) + 1 by NAT_1:13; then consider i being Nat such that A37: k+1 = len (P * FSeq) + 1 + i by NAT_1:10; thus seq2.(k+1) = Partial_Sums(P * ASeq).(len (P * FSeq)) by A30 ,A36 .= Partial_Sums(P * ASeq).(len FSeq) by Th61 .= Partial_Sums(P * ASeq).((len FSeq + 1) + i) by A18 .= Partial_Sums(P * ASeq).(k+1) by A37,Th61; end; end; hence thesis; end; seq2.0 = (P * ASeq).0 by A4,A30 .= Partial_Sums(P * ASeq).0 by SERIES_1:def 1; then A38: P[0]; A39: for k holds P[k] from NAT_1:sch 2(A38,A31); len (P * FSeq) <> 0 by A23,Th61; then seq2.(len (P * FSeq)) = Sum(P * FSeq) by A27,A30; hence Sum(P * FSeq) = Partial_Sums(P * ASeq).(len (P * FSeq)) by A39 .= Sum(P * ASeq) by A21,Th61; end; end; hence thesis; end; Partial_Sums(P * ASeq) is convergent by A19,Th3; then lim Partial_Sums(P * Partial_Diff_Union ASeq) <= lim Partial_Sums(P * ASeq) by A16,A15,SEQ_2:18; then Sum (P * Partial_Diff_Union ASeq) <= lim Partial_Sums(P * ASeq) by SERIES_1:def 3; then Sum (P * Partial_Diff_Union ASeq) <= Sum(P * ASeq) by SERIES_1:def 3; then P.(Union Partial_Diff_Union ASeq) <= Sum(P * ASeq) by Th46; hence thesis by A19,A20,A22,Th3,Th20,SERIES_1:def 3; end; theorem P.(Union FSeq) <= Sum(P * FSeq) & (FSeq is disjoint_valued implies P.( Union FSeq) = Sum(P * FSeq)) proof consider ASeq being SetSequence of Sigma such that A1: for k st k in dom FSeq holds ASeq.k = FSeq.k and A2: for k st not k in dom FSeq holds ASeq.k = {} by Th56; reconsider XSeq = ASeq as SetSequence of Omega; A3: (for k st k in dom FSeq holds XSeq.k = FSeq.k) & for k st not k in dom FSeq holds XSeq.k = {} by A1,A2; then P.(Union ASeq) = P.(Union FSeq) by Th55; then P.(Union FSeq) <= Sum(P * ASeq) by A1,A2,Th64; hence P.(Union FSeq) <= Sum(P * FSeq) by A1,A2,Th64; assume A4: FSeq is disjoint_valued; A5: FSeq is disjoint_valued implies ASeq is disjoint_valued proof assume A6: FSeq is disjoint_valued; for m,n being Nat st m <> n holds ASeq.m misses ASeq.n proof let m,n be Nat such that A7: m <> n; per cases; suppose A8: m in dom FSeq & n in dom FSeq; FSeq.m misses FSeq.n by A6,A7,PROB_2:def 2; then ASeq.m misses FSeq.n by A1,A8; hence thesis by A1,A8; end; suppose not (m in dom FSeq & n in dom FSeq); then ASeq.m = {} or ASeq.n = {} by A2; hence thesis; end; end; hence thesis; end; thus P.(Union FSeq) = P.(Union ASeq) by Th55,A3 .= Sum(P * ASeq) by A5,A4,Th46 .= Sum(P * FSeq) by A1,A2,Th64; end; definition ::$CD 2 let X; let IT be Subset-Family of X; attr IT is non-decreasing-closed means :Def7: for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds Union A1 in IT; attr IT is non-increasing-closed means :Def8: for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT holds Intersection A1 in IT; end; theorem Th66: for IT be Subset-Family of X holds IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds lim A1 in IT proof let IT be Subset-Family of X; thus IT is non-decreasing-closed implies for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds lim A1 in IT proof assume A1: IT is non-decreasing-closed; now let A1 be SetSequence of X; assume that A2: A1 is non-descending and A3: rng A1 c= IT; Union A1 in IT by A1,A2,A3; hence lim A1 in IT by A2,SETLIM_1:63; end; hence thesis; end; assume A4: for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds lim A1 in IT; for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds Union A1 in IT proof let A1 be SetSequence of X; assume that A5: A1 is non-descending and A6: rng A1 c= IT; lim A1 in IT by A4,A5,A6; hence thesis by A5,SETLIM_1:63; end; hence thesis; end; theorem Th67: for IT be Subset-Family of X holds IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT holds lim A1 in IT proof let IT be Subset-Family of X; thus IT is non-increasing-closed implies for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT holds lim A1 in IT proof assume A1: IT is non-increasing-closed; now let A1 be SetSequence of X; assume that A2: A1 is non-ascending and A3: rng A1 c= IT; Intersection A1 in IT by A1,A2,A3; hence lim A1 in IT by A2,SETLIM_1:64; end; hence thesis; end; assume A4: for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT holds lim A1 in IT; for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT holds Intersection A1 in IT proof let A1 be SetSequence of X; assume that A5: A1 is non-ascending and A6: rng A1 c= IT; lim A1 in IT by A4,A5,A6; hence thesis by A5,SETLIM_1:64; end; hence thesis; end; theorem Th68: bool X is non-decreasing-closed & bool X is non-increasing-closed; registration let X; cluster non-decreasing-closed non-increasing-closed for Subset-Family of X; existence proof take bool X; thus thesis; end; end; definition let X; mode MonotoneClass of X is non-decreasing-closed non-increasing-closed Subset-Family of X; end; theorem Th69: Z is MonotoneClass of X iff Z c= bool X & for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds lim A1 in Z proof thus Z is MonotoneClass of X implies Z c= bool X & for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds lim A1 in Z proof assume A1: Z is MonotoneClass of X; then reconsider Z as Subset-Family of X; for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds lim A1 in Z proof let A1 be SetSequence of X; assume that A2: A1 is monotone and A3: rng A1 c= Z; per cases by A2,SETLIM_1:def 1; suppose A1 is non-descending; hence thesis by A1,A3,Th66; end; suppose A1 is non-ascending; hence thesis by A1,A3,Th67; end; end; hence thesis; end; assume that A4: Z c= bool X and A5: for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds lim A1 in Z; reconsider Z as Subset-Family of X by A4; A6: for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= Z holds lim A1 in Z proof let A1 be SetSequence of X; assume A7: A1 is non-ascending & rng A1 c= Z; A1 is monotone & rng A1 c= Z implies lim A1 in Z by A5; hence thesis by A7,SETLIM_1:def 1; end; for A1 being SetSequence of X st A1 is non-descending & rng A1 c= Z holds lim A1 in Z proof let A1 be SetSequence of X; assume A8: A1 is non-descending & rng A1 c= Z; A1 is monotone & rng A1 c= Z implies lim A1 in Z by A5; hence thesis by A8,SETLIM_1:def 1; end; hence thesis by A6,Th66,Th67; end; theorem Th70: for F being Field_Subset of X holds F is SigmaField of X iff F is MonotoneClass of X proof let F be Field_Subset of X; thus F is SigmaField of X implies F is MonotoneClass of X proof assume F is SigmaField of X; then reconsider F as SigmaField of X; A1: for A1 being SetSequence of X st A1 is non-descending & rng A1 c= F holds Union A1 in F proof let A1 be SetSequence of X; assume that A1 is non-descending and A2: rng A1 c= F; reconsider A2=A1 as SetSequence of F by A2,RELAT_1:def 19; Union A2 in F by PROB_1:17; hence thesis; end; F is non-increasing-closed by PROB_1:def 6; hence thesis by A1,Def7; end; assume A3: F is MonotoneClass of X; for A1 being SetSequence of X st rng A1 c= F holds Intersection A1 in F proof let A1 such that A4: rng A1 c= F; set A2 = Partial_Intersection A1; defpred P[Nat] means A2.$1 in F; A5: for k st P[k] holds P[k+1] proof let k; assume A6: A2.k in F; A1.(k+1) in rng A1 & A2.(k+1) = A2.k /\ A1.(k+1) by Def1,NAT_1:51; hence A2.(k+1) in F by A4,A6,FINSUB_1:def 2; end; A1.0 in rng A1 & A2.0 = A1.0 by Def1,NAT_1:51; then A7: P[0] by A4; for k holds P[k] from NAT_1:sch 2(A7,A5); then A8: rng A2 c= F by NAT_1:52; A2 is non-ascending by Th10; then Intersection A2 in F by A3,A8,Def8; hence thesis by Th14; end; hence thesis by PROB_1:def 6; end; theorem bool Omega is MonotoneClass of Omega by Th68; definition let Omega; let X be Subset-Family of Omega; func monotoneclass(X) -> MonotoneClass of Omega means :Def9: X c= it & for Z st X c= Z & Z is MonotoneClass of Omega holds it c= Z; existence proof set V = { M where M is Subset-Family of Omega : X c= M & M is MonotoneClass of Omega}; set Y = meet V; A1: for Z st Z in V holds X c= Z proof let Z; assume Z in V; then ex M being Subset-Family of Omega st Z = M & X c= M & M is MonotoneClass of Omega; hence thesis; end; bool Omega is MonotoneClass of Omega by Th68; then A2: bool Omega in V; for MSeq being SetSequence of Omega st MSeq is monotone & rng MSeq c= Y holds lim MSeq in Y proof let MSeq be SetSequence of Omega such that A3: MSeq is monotone and A4: rng MSeq c= Y; now let Z; assume A5: Z in V; now let n be Nat; MSeq.n in rng MSeq by NAT_1:51; hence MSeq.n in Z by A4,A5,SETFAM_1:def 1; end; then A6: rng MSeq c= Z by NAT_1:52; ex M being Subset-Family of Omega st Z = M & X c= M & M is MonotoneClass of Omega by A5; hence lim MSeq in Z by A3,A6,Th69; end; hence thesis by A2,SETFAM_1:def 1; end; then reconsider Y as MonotoneClass of Omega by A2,Th69,SETFAM_1:3; take Y; for Z st X c= Z & Z is MonotoneClass of Omega holds Y c= Z proof let Z; assume X c= Z & Z is MonotoneClass of Omega; then Z in V; hence thesis by SETFAM_1:3; end; hence thesis by A2,A1,SETFAM_1:5; end; uniqueness; end; theorem Th72: for Z being Field_Subset of Omega holds monotoneclass(Z) is Field_Subset of Omega proof let Z be Field_Subset of Omega; A1: Z c= monotoneclass(Z) by Def9; then reconsider Z1=monotoneclass(Z) as non empty Subset-Family of Omega; A2: for y,Y being set st Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in Z1} for z being set st z in Y holds z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 proof let y,Y be set; assume A3: Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in Z1}; thus for z being set st z in Y holds z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 proof let z be set; assume z in Y; then ex z1 be Element of Z1 st z = z1 & y \ z1 in Z1 & z1 \ y in Z1 & z1 /\ y in Z1 by A3; hence thesis; end; end; A4: for y being Element of Z1,Y st Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in Z1} holds Y is MonotoneClass of Omega proof let y be Element of Z1,Y; assume A5: Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in Z1}; A6: for A1 being SetSequence of Omega st A1 is monotone & rng A1 c= Y holds lim A1 in Y proof let A1 be SetSequence of Omega such that A7: A1 is monotone and A8: rng A1 c= Y; A9: A1 is convergent by A7,SETLIM_1:65; for n holds A1.n in Z1 proof let n; A1.n in rng A1 by NAT_1:51; hence thesis by A2,A5,A8; end; then rng A1 c= Z1 by NAT_1:52; then A10: lim A1 is Element of Z1 by A7,Th69; for n holds (A1 (\) y).n in Z1 proof let n be Nat; A1.n in rng A1 by NAT_1:51; then n in NAT & A1.n \ y in Z1 by A2,A5,A8,ORDINAL1:def 12; hence thesis by SETLIM_2:def 8; end; then A11: rng(A1 (\) y) c= Z1 by NAT_1:52; for n holds (y (/\) A1).n in Z1 proof let n; A1.n in rng A1 by NAT_1:51; then n in NAT & y /\ A1.n in Z1 by A2,A5,A8,ORDINAL1:def 12; hence thesis by SETLIM_2:def 5; end; then A12: rng (y (/\) A1) c= Z1 by NAT_1:52; y (/\) A1 is monotone by A7,SETLIM_2:23; then lim (y (/\) A1) in Z1 by A12,Th69; then A13: y /\ lim A1 in Z1 by A9,SETLIM_2:92; for n holds (y (\) A1).n in Z1 proof let n; A1.n in rng A1 by NAT_1:51; then n in NAT & y \ A1.n in Z1 by A2,A5,A8,ORDINAL1:def 12; hence thesis by SETLIM_2:def 7; end; then A14: rng(y (\) A1) c= Z1 by NAT_1:52; y (\) A1 is monotone by A7,SETLIM_2:29; then lim (y (\) A1) in Z1 by A14,Th69; then A15: y \ lim A1 in Z1 by A9,SETLIM_2:94; A1 (\) y is monotone by A7,SETLIM_2:32; then lim (A1 (\) y) in Z1 by A11,Th69; then lim A1 \ y in Z1 by A9,SETLIM_2:95; hence thesis by A5,A10,A15,A13; end; for z being object holds z in Y implies z in Z1 by A2,A5; then Y c= Z1; hence thesis by A6,Th69,XBOOLE_1:1; end; A16: for y being Element of Z,Y st Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in Z1} holds Z1 c= Y proof let y be Element of Z,Y; assume A17: Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in Z1}; A18: Z c= Y proof let z be object; reconsider zz=z as set by TARSKI:1; assume A19: z in Z; then A20: zz /\ y in Z by FINSUB_1:def 2; zz \ y in Z & y \ zz in Z by A19,PROB_1:6; hence thesis by A1,A17,A19,A20; end; y in Z; then Y is MonotoneClass of Omega by A1,A4,A17; hence thesis by A18,Def9; end; A21: for y being Element of Z1,Y st Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in Z1} holds Z1 c= Y proof let y be Element of Z1,Y; assume A22: Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in Z1}; A23: Z c= Y proof let z be object; reconsider zz=z as set by TARSKI:1; set Y1 = {x where x is Element of Z1: zz \ x in Z1 & x \ zz in Z1 & x /\ zz in Z1}; assume A24: z in Z; then A25: Z1 c= Y1 by A16; A26: y in Z1; then A27: zz /\ y in Z1 by A2,A25; zz \ y in Z1 & y \ zz in Z1 by A2,A25,A26; hence thesis by A1,A22,A24,A27; end; Y is MonotoneClass of Omega by A4,A22; hence thesis by A23,Def9; end; A28: for y being Subset of Omega st y in Z1 holds y` in Z1 proof Omega in Z by PROB_1:5; then A29: Omega in Z1 by A1; let y be Subset of Omega such that A30: y in Z1; set Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in Z1}; Z1 c= Y by A21,A30; then Omega \ y in Z1 by A2,A29; hence thesis by SUBSET_1:def 4; end; now let y,z be set; assume that A31: y in Z1 and A32: z in Z1; set Y = {x where x is Element of Z1: y \ x in Z1 & x \ y in Z1 & x /\ y in Z1}; Z1 c= Y by A21,A31; hence y /\ z in Z1 by A2,A32; end; hence thesis by A28,FINSUB_1:def 2,PROB_1:def 1; end; theorem for Z being Field_Subset of Omega holds sigma Z = monotoneclass Z proof let Z be Field_Subset of Omega; monotoneclass Z is Field_Subset of Omega by Th72; then A1: monotoneclass Z is SigmaField of Omega by Th70; Z c= monotoneclass Z by Def9; hence sigma Z c= monotoneclass Z by A1,PROB_1:def 9; sigma Z is MonotoneClass of Omega & Z c= sigma Z by Th70,PROB_1:def 9; hence thesis by Def9; end;