:: PROB_3 semantic presentation begin Lm1: for t, p, s being real number st 0 < s & t <= p holds ( t < p + s & t - s < p ) proof let t, p, s be real number ; ::_thesis: ( 0 < s & t <= p implies ( t < p + s & t - s < p ) ) assume ( 0 < s & t <= p ) ; ::_thesis: ( t < p + s & t - s < p ) then t + 0 < p + s by XREAL_1:8; hence ( t < p + s & t - s < p ) by XREAL_1:19; ::_thesis: verum end; theorem Th1: :: PROB_3:1 for f being FinSequence holds not 0 in dom f proof let f be FinSequence; ::_thesis: not 0 in dom f assume 0 in dom f ; ::_thesis: contradiction then 0 in Seg (len f) by FINSEQ_1:def_3; hence contradiction by FINSEQ_1:1; ::_thesis: verum end; theorem Th2: :: PROB_3:2 for n being Nat for f being FinSequence holds ( n in dom f iff ( n <> 0 & n <= len f ) ) proof let n be Nat; ::_thesis: for f being FinSequence holds ( n in dom f iff ( n <> 0 & n <= len f ) ) let f be FinSequence; ::_thesis: ( n in dom f iff ( n <> 0 & n <= len f ) ) ( n in dom f iff ( n >= 1 & n <= len f ) ) by FINSEQ_3:25; hence ( n in dom f iff ( n <> 0 & n <= len f ) ) by NAT_1:14; ::_thesis: verum end; theorem Th3: :: PROB_3:3 for g being real number for f being Real_Sequence st ex k being Nat st for n being Nat st k <= n holds f . n = g holds ( f is convergent & lim f = g ) proof let g be real number ; ::_thesis: for f being Real_Sequence st ex k being Nat st for n being Nat st k <= n holds f . n = g holds ( f is convergent & lim f = g ) let f be Real_Sequence; ::_thesis: ( ex k being Nat st for n being Nat st k <= n holds f . n = g implies ( f is convergent & lim f = g ) ) given k being Nat such that A1: for n being Nat st k <= n holds f . n = g ; ::_thesis: ( f is convergent & lim f = g ) A2: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_ ex_k1_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k1_<=_m_holds_ abs_((f_._m)_-_g)_<_p reconsider k1 = k as Element of NAT by ORDINAL1:def_12; let p be real number ; ::_thesis: ( 0 < p implies ex k1 being Element of NAT st for m being Element of NAT st k1 <= m holds abs ((f . m) - g) < p ) assume A3: 0 < p ; ::_thesis: ex k1 being Element of NAT st for m being Element of NAT st k1 <= m holds abs ((f . m) - g) < p take k1 = k1; ::_thesis: for m being Element of NAT st k1 <= m holds abs ((f . m) - g) < p thus for m being Element of NAT st k1 <= m holds abs ((f . m) - g) < p ::_thesis: verum proof let m be Element of NAT ; ::_thesis: ( k1 <= m implies abs ((f . m) - g) < p ) assume k1 <= m ; ::_thesis: abs ((f . m) - g) < p then f . m = g by A1; hence abs ((f . m) - g) < p by A3, ABSVALUE:2; ::_thesis: verum end; end; hence f is convergent by SEQ_2:def_6; ::_thesis: lim f = g hence lim f = g by A2, SEQ_2:def_7; ::_thesis: verum end; theorem Th4: :: PROB_3:4 for n being Nat for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds (P * ASeq) . n >= 0 proof let n be Nat; ::_thesis: for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds (P * ASeq) . n >= 0 let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds (P * ASeq) . n >= 0 let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma holds (P * ASeq) . n >= 0 let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds (P * ASeq) . n >= 0 let P be Probability of Sigma; ::_thesis: (P * ASeq) . n >= 0 A1: n in NAT by ORDINAL1:def_12; then A2: ASeq . n is Event of Sigma by PROB_1:25; dom (P * ASeq) = NAT by SEQ_1:1; then (P * ASeq) . n = P . (ASeq . n) by A1, FUNCT_1:12; hence (P * ASeq) . n >= 0 by A2, PROB_1:def_8; ::_thesis: verum end; theorem Th5: :: PROB_3:5 for n being Nat for Omega being non empty set for Sigma being SigmaField of Omega for ASeq, BSeq being SetSequence of Sigma for P being Probability of Sigma st ASeq . n c= BSeq . n holds (P * ASeq) . n <= (P * BSeq) . n proof let n be Nat; ::_thesis: for Omega being non empty set for Sigma being SigmaField of Omega for ASeq, BSeq being SetSequence of Sigma for P being Probability of Sigma st ASeq . n c= BSeq . n holds (P * ASeq) . n <= (P * BSeq) . n let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq, BSeq being SetSequence of Sigma for P being Probability of Sigma st ASeq . n c= BSeq . n holds (P * ASeq) . n <= (P * BSeq) . n let Sigma be SigmaField of Omega; ::_thesis: for ASeq, BSeq being SetSequence of Sigma for P being Probability of Sigma st ASeq . n c= BSeq . n holds (P * ASeq) . n <= (P * BSeq) . n let ASeq, BSeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq . n c= BSeq . n holds (P * ASeq) . n <= (P * BSeq) . n let P be Probability of Sigma; ::_thesis: ( ASeq . n c= BSeq . n implies (P * ASeq) . n <= (P * BSeq) . n ) A1: n in NAT by ORDINAL1:def_12; A2: ( ASeq . n in rng ASeq & BSeq . n in rng BSeq ) by NAT_1:51; assume ASeq . n c= BSeq . n ; ::_thesis: (P * ASeq) . n <= (P * BSeq) . n then P . (ASeq . n) <= P . (BSeq . n) by A2, PROB_1:34; then (P * ASeq) . n <= P . (BSeq . n) by A1, FUNCT_2:15; hence (P * ASeq) . n <= (P * BSeq) . n by A1, FUNCT_2:15; ::_thesis: verum end; theorem Th6: :: PROB_3:6 for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V71() holds P * ASeq is non-decreasing proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V71() holds P * ASeq is non-decreasing let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V71() holds P * ASeq is non-decreasing let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq is V71() holds P * ASeq is non-decreasing let P be Probability of Sigma; ::_thesis: ( ASeq is V71() implies P * ASeq is non-decreasing ) A1: dom (P * ASeq) = NAT by SEQ_1:1; assume A2: ASeq is V71() ; ::_thesis: P * ASeq is non-decreasing now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ (P_*_ASeq)_._n_<=_(P_*_ASeq)_._m let n, m be Element of NAT ; ::_thesis: ( n <= m implies (P * ASeq) . n <= (P * ASeq) . m ) assume n <= m ; ::_thesis: (P * ASeq) . n <= (P * ASeq) . m then A3: ASeq . n c= ASeq . m by A2, PROB_1:def_5; ( (P * ASeq) . n = P . (ASeq . n) & (P * ASeq) . m = P . (ASeq . m) ) by A1, FUNCT_1:12; hence (P * ASeq) . n <= (P * ASeq) . m by A3, PROB_1:34; ::_thesis: verum end; hence P * ASeq is non-decreasing by SEQM_3:6; ::_thesis: verum end; theorem Th7: :: PROB_3:7 for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V70() holds P * ASeq is non-increasing proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V70() holds P * ASeq is non-increasing let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V70() holds P * ASeq is non-increasing let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq is V70() holds P * ASeq is non-increasing let P be Probability of Sigma; ::_thesis: ( ASeq is V70() implies P * ASeq is non-increasing ) A1: dom (P * ASeq) = NAT by SEQ_1:1; assume A2: ASeq is V70() ; ::_thesis: P * ASeq is non-increasing now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ (P_*_ASeq)_._m_<=_(P_*_ASeq)_._n let n, m be Element of NAT ; ::_thesis: ( n <= m implies (P * ASeq) . m <= (P * ASeq) . n ) assume n <= m ; ::_thesis: (P * ASeq) . m <= (P * ASeq) . n then A3: ASeq . m c= ASeq . n by A2, PROB_1:def_4; ( (P * ASeq) . n = P . (ASeq . n) & (P * ASeq) . m = P . (ASeq . m) ) by A1, FUNCT_1:12; hence (P * ASeq) . m <= (P * ASeq) . n by A3, PROB_1:34; ::_thesis: verum end; hence P * ASeq is non-increasing by SEQM_3:8; ::_thesis: verum end; definition let X be set ; let A1 be SetSequence of X; func Partial_Intersection A1 -> SetSequence of X means :Def1: :: PROB_3:def 1 ( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (it . n) /\ (A1 . (n + 1)) ) ); existence ex b1 being SetSequence of X st ( b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) /\ (A1 . (n + 1)) ) ) proof defpred S1[ set , set , set ] means for x, y being Subset of X for s being Nat st s = $1 & x = $2 & y = $3 holds y = x /\ (A1 . (s + 1)); A1: for n being Element of NAT for x being Subset of X ex y being Subset of X st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Subset of X ex y being Subset of X st S1[n,x,y] let x be Subset of X; ::_thesis: ex y being Subset of X st S1[n,x,y] take x /\ (A1 . (n + 1)) ; ::_thesis: S1[n,x,x /\ (A1 . (n + 1))] thus S1[n,x,x /\ (A1 . (n + 1))] ; ::_thesis: verum end; consider F being SetSequence of X such that A2: F . 0 = A1 . 0 and A3: for n being Element of NAT holds S1[n,F . n,F . (n + 1)] from RECDEF_1:sch_2(A1); take F ; ::_thesis: ( F . 0 = A1 . 0 & ( for n being Nat holds F . (n + 1) = (F . n) /\ (A1 . (n + 1)) ) ) thus F . 0 = A1 . 0 by A2; ::_thesis: for n being Nat holds F . (n + 1) = (F . n) /\ (A1 . (n + 1)) let n be Nat; ::_thesis: F . (n + 1) = (F . n) /\ (A1 . (n + 1)) reconsider n = n as Element of NAT by ORDINAL1:def_12; S1[n,F . n,F . (n + 1)] by A3; hence F . (n + 1) = (F . n) /\ (A1 . (n + 1)) ; ::_thesis: verum end; uniqueness for b1, b2 being SetSequence of X st b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) /\ (A1 . (n + 1)) ) & b2 . 0 = A1 . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) /\ (A1 . (n + 1)) ) holds b1 = b2 proof let S1, S2 be SetSequence of X; ::_thesis: ( S1 . 0 = A1 . 0 & ( for n being Nat holds S1 . (n + 1) = (S1 . n) /\ (A1 . (n + 1)) ) & S2 . 0 = A1 . 0 & ( for n being Nat holds S2 . (n + 1) = (S2 . n) /\ (A1 . (n + 1)) ) implies S1 = S2 ) assume 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)) ; ::_thesis: S1 = S2 defpred S1[ set ] means S1 . $1 = S2 . $1; for n being set st n in NAT holds S1[n] proof let n be set ; ::_thesis: ( n in NAT implies S1[n] ) assume n in NAT ; ::_thesis: S1[n] then reconsider n = n as Element of NAT ; A8: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1 . k = S2 . k ; ::_thesis: S1[k + 1] hence S1 . (k + 1) = (S2 . k) /\ (A1 . (k + 1)) by A5 .= S2 . (k + 1) by A7 ; ::_thesis: verum end; A9: S1[ 0 ] by A4, A6; for k being Nat holds S1[k] from NAT_1:sch_2(A9, A8); then S1 . n = S2 . n ; hence S1[n] ; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def1 defines Partial_Intersection PROB_3:def_1_:_ for X being set for A1, b3 being SetSequence of X holds ( b3 = Partial_Intersection A1 iff ( b3 . 0 = A1 . 0 & ( for n being Nat holds b3 . (n + 1) = (b3 . n) /\ (A1 . (n + 1)) ) ) ); definition let X be set ; let A1 be SetSequence of X; func Partial_Union A1 -> SetSequence of X means :Def2: :: PROB_3:def 2 ( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (it . n) \/ (A1 . (n + 1)) ) ); existence ex b1 being SetSequence of X st ( b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) \/ (A1 . (n + 1)) ) ) proof defpred S1[ set , set , set ] means for x, y being Subset of X for s being Nat st s = $1 & x = $2 & y = $3 holds y = x \/ (A1 . (s + 1)); A1: for n being Element of NAT for x being Subset of X ex y being Subset of X st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Subset of X ex y being Subset of X st S1[n,x,y] let x be Subset of X; ::_thesis: ex y being Subset of X st S1[n,x,y] take x \/ (A1 . (n + 1)) ; ::_thesis: S1[n,x,x \/ (A1 . (n + 1))] thus S1[n,x,x \/ (A1 . (n + 1))] ; ::_thesis: verum end; consider F being SetSequence of X such that A2: F . 0 = A1 . 0 and A3: for n being Element of NAT holds S1[n,F . n,F . (n + 1)] from RECDEF_1:sch_2(A1); take F ; ::_thesis: ( F . 0 = A1 . 0 & ( for n being Nat holds F . (n + 1) = (F . n) \/ (A1 . (n + 1)) ) ) thus F . 0 = A1 . 0 by A2; ::_thesis: for n being Nat holds F . (n + 1) = (F . n) \/ (A1 . (n + 1)) let n be Nat; ::_thesis: F . (n + 1) = (F . n) \/ (A1 . (n + 1)) reconsider n = n as Element of NAT by ORDINAL1:def_12; S1[n,F . n,F . (n + 1)] by A3; hence F . (n + 1) = (F . n) \/ (A1 . (n + 1)) ; ::_thesis: verum end; uniqueness for b1, b2 being SetSequence of X st b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) \/ (A1 . (n + 1)) ) & b2 . 0 = A1 . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) \/ (A1 . (n + 1)) ) holds b1 = b2 proof let S1, S2 be SetSequence of X; ::_thesis: ( S1 . 0 = A1 . 0 & ( for n being Nat holds S1 . (n + 1) = (S1 . n) \/ (A1 . (n + 1)) ) & S2 . 0 = A1 . 0 & ( for n being Nat holds S2 . (n + 1) = (S2 . n) \/ (A1 . (n + 1)) ) implies S1 = S2 ) assume 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)) ; ::_thesis: S1 = S2 defpred S1[ set ] means S1 . $1 = S2 . $1; for n being set st n in NAT holds S1[n] proof let n be set ; ::_thesis: ( n in NAT implies S1[n] ) assume n in NAT ; ::_thesis: S1[n] then reconsider n = n as Element of NAT ; A8: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1 . k = S2 . k ; ::_thesis: S1[k + 1] hence S1 . (k + 1) = (S2 . k) \/ (A1 . (k + 1)) by A5 .= S2 . (k + 1) by A7 ; ::_thesis: verum end; A9: S1[ 0 ] by A4, A6; for k being Nat holds S1[k] from NAT_1:sch_2(A9, A8); then S1 . n = S2 . n ; hence S1[n] ; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def2 defines Partial_Union PROB_3:def_2_:_ for X being set for A1, b3 being SetSequence of X holds ( b3 = Partial_Union A1 iff ( b3 . 0 = A1 . 0 & ( for n being Nat holds b3 . (n + 1) = (b3 . n) \/ (A1 . (n + 1)) ) ) ); theorem Th8: :: PROB_3:8 for n being Nat for X being set for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n proof let n be Nat; ::_thesis: for X being set for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n let X be set ; ::_thesis: for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n let A1 be SetSequence of X; ::_thesis: (Partial_Intersection A1) . n c= A1 . n percases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6; suppose n = 0 ; ::_thesis: (Partial_Intersection A1) . n c= A1 . n hence (Partial_Intersection A1) . n c= A1 . n by Def1; ::_thesis: verum end; suppose ex k being Nat st n = k + 1 ; ::_thesis: (Partial_Intersection A1) . n c= A1 . n then consider k being Nat such that A1: n = k + 1 ; (Partial_Intersection A1) . (k + 1) = ((Partial_Intersection A1) . k) /\ (A1 . (k + 1)) by Def1; hence (Partial_Intersection A1) . n c= A1 . n by A1, XBOOLE_1:17; ::_thesis: verum end; end; end; theorem Th9: :: PROB_3:9 for n being Nat for X being set for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n proof let n be Nat; ::_thesis: for X being set for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n let X be set ; ::_thesis: for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n let A1 be SetSequence of X; ::_thesis: A1 . n c= (Partial_Union A1) . n percases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6; suppose n = 0 ; ::_thesis: A1 . n c= (Partial_Union A1) . n hence A1 . n c= (Partial_Union A1) . n by Def2; ::_thesis: verum end; suppose ex k being Nat st n = k + 1 ; ::_thesis: A1 . n c= (Partial_Union A1) . n then consider k being Nat such that A1: n = k + 1 ; (Partial_Union A1) . (k + 1) = ((Partial_Union A1) . k) \/ (A1 . (k + 1)) by Def2; hence A1 . n c= (Partial_Union A1) . n by A1, XBOOLE_1:7; ::_thesis: verum end; end; end; theorem Th10: :: PROB_3:10 for X being set for A1 being SetSequence of X holds Partial_Intersection A1 is V70() proof let X be set ; ::_thesis: for A1 being SetSequence of X holds Partial_Intersection A1 is V70() let A1 be SetSequence of X; ::_thesis: Partial_Intersection A1 is V70() now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Intersection_A1)_._(n_+_1)_c=_(Partial_Intersection_A1)_._n let n be Element of NAT ; ::_thesis: (Partial_Intersection A1) . (n + 1) c= (Partial_Intersection A1) . n (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; ::_thesis: verum end; hence Partial_Intersection A1 is V70() by PROB_2:6; ::_thesis: verum end; theorem Th11: :: PROB_3:11 for X being set for A1 being SetSequence of X holds Partial_Union A1 is V71() proof let X be set ; ::_thesis: for A1 being SetSequence of X holds Partial_Union A1 is V71() let A1 be SetSequence of X; ::_thesis: Partial_Union A1 is V71() now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Union_A1)_._n_c=_(Partial_Union_A1)_._(n_+_1) let n be Element of NAT ; ::_thesis: (Partial_Union A1) . n c= (Partial_Union A1) . (n + 1) (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; ::_thesis: verum end; hence Partial_Union A1 is V71() by PROB_2:7; ::_thesis: verum end; theorem Th12: :: PROB_3:12 for n being Nat for X, x being set for A1 being SetSequence of X holds ( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds x in A1 . k ) proof let n be Nat; ::_thesis: for X, x being set for A1 being SetSequence of X holds ( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds x in A1 . k ) let X, x be set ; ::_thesis: for A1 being SetSequence of X holds ( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds x in A1 . k ) let A1 be SetSequence of X; ::_thesis: ( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds x in A1 . k ) defpred S1[ Nat] means ( ( for k being Nat st k <= $1 holds x in A1 . k ) implies x in (Partial_Intersection A1) . $1 ); A1: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A2: ( ( for k being Nat st k <= i holds x in A1 . k ) implies x in (Partial_Intersection A1) . i ) ; ::_thesis: S1[i + 1] assume for k being Nat st k <= i + 1 holds x in A1 . k ; ::_thesis: x in (Partial_Intersection A1) . (i + 1) then A3: ( ( for k being Nat 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 x in (Partial_Intersection A1) . (i + 1) by A2, A3, XBOOLE_0:def_4; ::_thesis: verum end; thus ( x in (Partial_Intersection A1) . n implies for k being Nat st k <= n holds x in A1 . k ) ::_thesis: ( ( for k being Nat st k <= n holds x in A1 . k ) implies x in (Partial_Intersection A1) . n ) proof assume A4: x in (Partial_Intersection A1) . n ; ::_thesis: for k being Nat st k <= n holds x in A1 . k for k being Nat st k <= n holds x in A1 . k proof A5: Partial_Intersection A1 is V70() by Th10; let k be Nat; ::_thesis: ( k <= n implies x in A1 . k ) assume A6: k <= n ; ::_thesis: x in A1 . k A7: (Partial_Intersection A1) . k c= A1 . k by Th8; ( n in NAT & k in NAT ) by ORDINAL1:def_12; then (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, XBOOLE_1:1; hence x in A1 . k by A4; ::_thesis: verum end; hence for k being Nat st k <= n holds x in A1 . k ; ::_thesis: verum end; A8: S1[ 0 ] proof assume for k being Nat st k <= 0 holds x in A1 . k ; ::_thesis: x in (Partial_Intersection A1) . 0 then x in A1 . 0 ; hence x in (Partial_Intersection A1) . 0 by Def1; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A8, A1); hence ( ( for k being Nat st k <= n holds x in A1 . k ) implies x in (Partial_Intersection A1) . n ) ; ::_thesis: verum end; theorem Th13: :: PROB_3:13 for n being Nat for X, x being set for A1 being SetSequence of X holds ( x in (Partial_Union A1) . n iff ex k being Nat st ( k <= n & x in A1 . k ) ) proof let n be Nat; ::_thesis: for X, x being set for A1 being SetSequence of X holds ( x in (Partial_Union A1) . n iff ex k being Nat st ( k <= n & x in A1 . k ) ) let X, x be set ; ::_thesis: for A1 being SetSequence of X holds ( x in (Partial_Union A1) . n iff ex k being Nat st ( k <= n & x in A1 . k ) ) let A1 be SetSequence of X; ::_thesis: ( x in (Partial_Union A1) . n iff ex k being Nat st ( k <= n & x in A1 . k ) ) defpred S1[ Nat] means ( x in (Partial_Union A1) . $1 implies ex k being Nat st ( k <= $1 & x in A1 . k ) ); A1: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A2: ( x in (Partial_Union A1) . i implies ex k being Nat st ( k <= i & x in A1 . k ) ) ; ::_thesis: S1[i + 1] assume A3: x in (Partial_Union A1) . (i + 1) ; ::_thesis: ex k being Nat st ( k <= i + 1 & x in A1 . k ) A4: (Partial_Union A1) . (i + 1) = ((Partial_Union A1) . i) \/ (A1 . (i + 1)) by Def2; now__::_thesis:_(_(_x_in_(Partial_Union_A1)_._i_&_ex_k,_k_being_Nat_st_ (_k_<=_i_+_1_&_x_in_A1_._k_)_)_or_(_x_in_A1_._(i_+_1)_&_ex_k_being_Nat_st_ (_k_<=_i_+_1_&_x_in_A1_._k_)_)_) percases ( x in (Partial_Union A1) . i or x in A1 . (i + 1) ) by A3, A4, XBOOLE_0:def_3; case x in (Partial_Union A1) . i ; ::_thesis: ex k, k being Nat st ( k <= i + 1 & x in A1 . k ) then consider k being Nat such that A5: ( k <= i & x in A1 . k ) by A2; take k = k; ::_thesis: ex k being Nat st ( k <= i + 1 & x in A1 . k ) thus ex k being Nat st ( k <= i + 1 & x in A1 . k ) by A5, NAT_1:12; ::_thesis: verum end; case x in A1 . (i + 1) ; ::_thesis: ex k being Nat st ( k <= i + 1 & x in A1 . k ) hence ex k being Nat st ( k <= i + 1 & x in A1 . k ) ; ::_thesis: verum end; end; end; hence ex k being Nat st ( k <= i + 1 & x in A1 . k ) ; ::_thesis: verum end; A6: S1[ 0 ] proof assume A7: x in (Partial_Union A1) . 0 ; ::_thesis: ex k being Nat st ( k <= 0 & x in A1 . k ) take 0 ; ::_thesis: ( 0 <= 0 & x in A1 . 0 ) thus ( 0 <= 0 & x in A1 . 0 ) by A7, Def2; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A6, A1); hence ( x in (Partial_Union A1) . n implies ex k being Nat st ( k <= n & x in A1 . k ) ) ; ::_thesis: ( ex k being Nat st ( k <= n & x in A1 . k ) implies x in (Partial_Union A1) . n ) given i being Nat such that A8: i <= n and A9: x in A1 . i ; ::_thesis: x in (Partial_Union A1) . n A1 . i c= (Partial_Union A1) . i by Th9; then A10: x in (Partial_Union A1) . i by A9; A11: Partial_Union A1 is V71() by Th11; ( n in NAT & i in NAT ) by ORDINAL1:def_12; then (Partial_Union A1) . i c= (Partial_Union A1) . n by A8, A11, PROB_1:def_5; hence x in (Partial_Union A1) . n by A10; ::_thesis: verum end; theorem Th14: :: PROB_3:14 for X being set for A1 being SetSequence of X holds Intersection (Partial_Intersection A1) = Intersection A1 proof let X be set ; ::_thesis: for A1 being SetSequence of X holds Intersection (Partial_Intersection A1) = Intersection A1 let A1 be SetSequence of X; ::_thesis: Intersection (Partial_Intersection A1) = Intersection A1 thus Intersection (Partial_Intersection A1) c= Intersection A1 :: according to XBOOLE_0:def_10 ::_thesis: Intersection A1 c= Intersection (Partial_Intersection A1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection (Partial_Intersection A1) or x in Intersection A1 ) assume A1: x in Intersection (Partial_Intersection A1) ; ::_thesis: x in Intersection A1 for n being Element of NAT holds x in A1 . n proof let n be Element of NAT ; ::_thesis: x in A1 . n x in (Partial_Intersection A1) . n by A1, PROB_1:13; hence x in A1 . n by Th12; ::_thesis: verum end; hence x in Intersection A1 by PROB_1:13; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection A1 or x in Intersection (Partial_Intersection A1) ) assume A2: x in Intersection A1 ; ::_thesis: x in Intersection (Partial_Intersection A1) for n being Element of NAT holds x in (Partial_Intersection A1) . n proof let n be Element of NAT ; ::_thesis: x in (Partial_Intersection A1) . n for k being Nat st k <= n holds x in A1 . k proof let k be Nat; ::_thesis: ( k <= n implies x in A1 . k ) k in NAT by ORDINAL1:def_12; hence ( k <= n implies x in A1 . k ) by A2, PROB_1:13; ::_thesis: verum end; hence x in (Partial_Intersection A1) . n by Th12; ::_thesis: verum end; hence x in Intersection (Partial_Intersection A1) by PROB_1:13; ::_thesis: verum end; theorem Th15: :: PROB_3:15 for X being set for A1 being SetSequence of X holds Union (Partial_Union A1) = Union A1 proof let X be set ; ::_thesis: for A1 being SetSequence of X holds Union (Partial_Union A1) = Union A1 let A1 be SetSequence of X; ::_thesis: Union (Partial_Union A1) = Union A1 thus Union (Partial_Union A1) c= Union A1 :: according to XBOOLE_0:def_10 ::_thesis: Union A1 c= Union (Partial_Union A1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (Partial_Union A1) or x in Union A1 ) assume x in Union (Partial_Union A1) ; ::_thesis: x in Union A1 then consider n being Element of NAT such that A1: x in (Partial_Union A1) . n by PROB_1:12; consider k being Nat such that k <= n and A2: x in A1 . k by A1, Th13; k in NAT by ORDINAL1:def_12; hence x in Union A1 by A2, PROB_1:12; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union A1 or x in Union (Partial_Union A1) ) assume x in Union A1 ; ::_thesis: x in Union (Partial_Union A1) then consider n being Element of NAT such that A3: x in A1 . n by PROB_1:12; x in (Partial_Union A1) . n by A3, Th13; hence x in Union (Partial_Union A1) by PROB_1:12; ::_thesis: verum end; definition let X be set ; let A1 be SetSequence of X; func Partial_Diff_Union A1 -> SetSequence of X means :Def3: :: PROB_3:def 3 ( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) ); existence ex b1 being SetSequence of X st ( b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) ) proof defpred S1[ set , set , set ] means for x, y being Subset of X for s being Nat st s = $1 & x = $2 & y = $3 holds y = (A1 . (s + 1)) \ ((Partial_Union A1) . s); set A = A1 . 0; A1: for n being Element of NAT for x being Subset of X ex y being Subset of X st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Subset of X ex y being Subset of X st S1[n,x,y] let x be Subset of X; ::_thesis: ex y being Subset of X st S1[n,x,y] take (A1 . (n + 1)) \ ((Partial_Union A1) . n) ; ::_thesis: S1[n,x,(A1 . (n + 1)) \ ((Partial_Union A1) . n)] thus S1[n,x,(A1 . (n + 1)) \ ((Partial_Union A1) . n)] ; ::_thesis: verum end; consider F being SetSequence of X such that A2: ( F . 0 = A1 . 0 & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A1); for n being Nat holds F . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) proof let n be Nat; ::_thesis: F . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) reconsider n1 = n as Element of NAT by ORDINAL1:def_12; for x, y being Subset of X for s being Nat st s = n1 & x = F . n1 & y = F . (n1 + 1) holds y = (A1 . (s + 1)) \ ((Partial_Union A1) . s) by A2; hence F . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ; ::_thesis: verum end; hence ex b1 being SetSequence of X st ( b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being SetSequence of X st b1 . 0 = A1 . 0 & ( for n being Nat holds b1 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) & b2 . 0 = A1 . 0 & ( for n being Nat holds b2 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) holds b1 = b2 proof let S1, S2 be SetSequence of X; ::_thesis: ( S1 . 0 = A1 . 0 & ( for n being Nat holds S1 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) & S2 . 0 = A1 . 0 & ( for n being Nat holds S2 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) implies S1 = S2 ) assume 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) ; ::_thesis: S1 = S2 defpred S1[ set ] means S1 . $1 = S2 . $1; for n being set st n in NAT holds S1[n] proof let n be set ; ::_thesis: ( n in NAT implies S1[n] ) assume n in NAT ; ::_thesis: S1[n] then reconsider n = n as Element of NAT ; A7: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1 . k = S2 . k ; ::_thesis: S1[k + 1] thus S1 . (k + 1) = (A1 . (k + 1)) \ ((Partial_Union A1) . k) by A4 .= S2 . (k + 1) by A6 ; ::_thesis: verum end; A8: S1[ 0 ] by A3, A5; for k being Nat holds S1[k] from NAT_1:sch_2(A8, A7); then S1 . n = S2 . n ; hence S1[n] ; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def3 defines Partial_Diff_Union PROB_3:def_3_:_ for X being set for A1, b3 being SetSequence of X holds ( b3 = Partial_Diff_Union A1 iff ( b3 . 0 = A1 . 0 & ( for n being Nat holds b3 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) ) ); theorem Th16: :: PROB_3:16 for n being Nat for X, x being set for A1 being SetSequence of X holds ( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) ) ) proof let n be Nat; ::_thesis: for X, x being set for A1 being SetSequence of X holds ( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) ) ) let X, x be set ; ::_thesis: for A1 being SetSequence of X holds ( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) ) ) let A1 be SetSequence of X; ::_thesis: ( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) ) ) thus ( x in (Partial_Diff_Union A1) . n implies ( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) ) ) ::_thesis: ( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) implies x in (Partial_Diff_Union A1) . n ) proof assume A1: x in (Partial_Diff_Union A1) . n ; ::_thesis: ( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) ) now__::_thesis:_(_(_n_=_0_&_x_in_A1_._n_&_(_for_k_being_Nat_st_k_<_n_holds_ not_x_in_A1_._k_)_)_or_(_ex_n1_being_Nat_st_n_=_n1_+_1_&_x_in_A1_._n_&_(_for_k_being_Nat_st_k_<_n_holds_ not_x_in_A1_._k_)_)_) percases ( n = 0 or ex n1 being Nat st n = n1 + 1 ) by NAT_1:6; case n = 0 ; ::_thesis: ( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) ) hence ( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) ) by A1, Def3, NAT_1:2; ::_thesis: verum end; case ex n1 being Nat st n = n1 + 1 ; ::_thesis: ( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) ) 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 being Nat st k < n holds not x in A1 . k proof let k be Nat; ::_thesis: ( k < n implies not x in A1 . k ) assume k < n ; ::_thesis: not x in A1 . k then k <= n1 by A2, NAT_1:13; hence not x in A1 . k by A4, Th13; ::_thesis: verum end; hence ( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) ) by A2, A3, XBOOLE_0:def_5; ::_thesis: verum end; end; end; hence ( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) ) ; ::_thesis: verum end; assume that A5: x in A1 . n and A6: for k being Nat st k < n holds not x in A1 . k ; ::_thesis: x in (Partial_Diff_Union A1) . n now__::_thesis:_(_(_n_=_0_&_x_in_(Partial_Diff_Union_A1)_._n_)_or_(_ex_n1_being_Nat_st_n_=_n1_+_1_&_x_in_(Partial_Diff_Union_A1)_._n_)_) percases ( n = 0 or ex n1 being Nat st n = n1 + 1 ) by NAT_1:6; case n = 0 ; ::_thesis: x in (Partial_Diff_Union A1) . n hence x in (Partial_Diff_Union A1) . n by A5, Def3; ::_thesis: verum end; case ex n1 being Nat st n = n1 + 1 ; ::_thesis: x in (Partial_Diff_Union A1) . n then consider n1 being Nat such that A7: n = n1 + 1 ; for k being Nat st k <= n1 holds not x in A1 . k proof let k be Nat; ::_thesis: ( k <= n1 implies not x in A1 . k ) assume k <= n1 ; ::_thesis: not x in A1 . k then k < n1 + 1 by NAT_1:13; hence not x in A1 . k by A6, A7; ::_thesis: verum 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 x in (Partial_Diff_Union A1) . n by A7, Def3; ::_thesis: verum end; end; end; hence x in (Partial_Diff_Union A1) . n ; ::_thesis: verum end; theorem Th17: :: PROB_3:17 for n being Nat for X being set for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= A1 . n proof let n be Nat; ::_thesis: for X being set for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= A1 . n let X be set ; ::_thesis: for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= A1 . n let A1 be SetSequence of X; ::_thesis: (Partial_Diff_Union A1) . n c= A1 . n for x being set st x in (Partial_Diff_Union A1) . n holds x in A1 . n by Th16; hence (Partial_Diff_Union A1) . n c= A1 . n by TARSKI:def_3; ::_thesis: verum end; theorem Th18: :: PROB_3:18 for n being Nat for X being set for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n proof let n be Nat; ::_thesis: for X being set for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n let X be set ; ::_thesis: for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n let A1 be SetSequence of X; ::_thesis: (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n ( (Partial_Diff_Union A1) . n c= A1 . n & A1 . n c= (Partial_Union A1) . n ) by Th9, Th17; hence (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n by XBOOLE_1:1; ::_thesis: verum end; theorem Th19: :: PROB_3:19 for X being set for A1 being SetSequence of X holds Partial_Union (Partial_Diff_Union A1) = Partial_Union A1 proof let X be set ; ::_thesis: for A1 being SetSequence of X holds Partial_Union (Partial_Diff_Union A1) = Partial_Union A1 let A1 be SetSequence of X; ::_thesis: Partial_Union (Partial_Diff_Union A1) = Partial_Union A1 for n being Element of NAT holds (Partial_Union (Partial_Diff_Union A1)) . n = (Partial_Union A1) . n proof set A2 = Partial_Diff_Union A1; defpred S1[ set ] means (Partial_Union (Partial_Diff_Union A1)) . $1 = (Partial_Union A1) . $1; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: (Partial_Union (Partial_Diff_Union A1)) . k = (Partial_Union A1) . k ; ::_thesis: S1[k + 1] thus (Partial_Union (Partial_Diff_Union A1)) . (k + 1) = ((Partial_Diff_Union A1) . (k + 1)) \/ ((Partial_Union (Partial_Diff_Union A1)) . 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 ; ::_thesis: verum end; (Partial_Union (Partial_Diff_Union A1)) . 0 = (Partial_Diff_Union A1) . 0 by Def2 .= A1 . 0 by Def3 .= (Partial_Union A1) . 0 by Def2 ; then A3: S1[ 0 ] ; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); ::_thesis: verum end; hence Partial_Union (Partial_Diff_Union A1) = Partial_Union A1 by FUNCT_2:63; ::_thesis: verum end; theorem Th20: :: PROB_3:20 for X being set for A1 being SetSequence of X holds Union (Partial_Diff_Union A1) = Union A1 proof let X be set ; ::_thesis: for A1 being SetSequence of X holds Union (Partial_Diff_Union A1) = Union A1 let A1 be SetSequence of X; ::_thesis: Union (Partial_Diff_Union A1) = Union A1 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 ; ::_thesis: verum end; definition let X be set ; let A1 be SetSequence of X; :: original: disjoint_valued redefine attrA1 is disjoint_valued means :Def4: :: PROB_3:def 4 for m, n being Nat st m <> n holds A1 . m misses A1 . n; compatibility ( A1 is disjoint_valued iff for m, n being Nat st m <> n holds A1 . m misses A1 . n ) proof thus ( A1 is V73() implies for m, n being Nat st m <> n holds A1 . m misses A1 . n ) by PROB_2:def_2; ::_thesis: ( ( for m, n being Nat st m <> n holds A1 . m misses A1 . n ) implies A1 is disjoint_valued ) assume A1: for m, n being Nat st m <> n holds A1 . m misses A1 . n ; ::_thesis: A1 is disjoint_valued now__::_thesis:_for_x,_y_being_set_st_x_<>_y_holds_ A1_._x_misses_A1_._y let x, y be set ; ::_thesis: ( x <> y implies A1 . b1 misses A1 . b2 ) assume A2: x <> y ; ::_thesis: A1 . b1 misses A1 . b2 percases ( ( x in dom A1 & y in dom A1 ) or not x in dom A1 or not y in dom A1 ) ; suppose ( x in dom A1 & y in dom A1 ) ; ::_thesis: A1 . b1 misses A1 . b2 hence A1 . x misses A1 . y by A1, A2; ::_thesis: verum end; suppose ( not x in dom A1 or not y in dom A1 ) ; ::_thesis: A1 . b1 misses A1 . b2 then ( A1 . x = {} or A1 . y = {} ) by FUNCT_1:def_2; hence A1 . x misses A1 . y by XBOOLE_1:65; ::_thesis: verum end; end; end; hence A1 is disjoint_valued by PROB_2:def_2; ::_thesis: verum end; end; :: deftheorem Def4 defines disjoint_valued PROB_3:def_4_:_ for X being set for A1 being SetSequence of X holds ( A1 is disjoint_valued iff for m, n being Nat st m <> n holds A1 . m misses A1 . n ); registration let X be set ; let A1 be SetSequence of X; cluster Partial_Diff_Union A1 -> V73() ; coherence Partial_Diff_Union A1 is disjoint_valued proof for m, n being Nat st m <> n holds (Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m proof let m, n be Nat; ::_thesis: ( m <> n implies (Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m ) assume A1: m <> n ; ::_thesis: (Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m assume (Partial_Diff_Union A1) . n meets (Partial_Diff_Union A1) . m ; ::_thesis: contradiction then consider x being set such that A2: x in (Partial_Diff_Union A1) . n and A3: x in (Partial_Diff_Union A1) . m by XBOOLE_0:3; percases ( m < n or n < m ) by A1, XXREAL_0:1; suppose m < n ; ::_thesis: contradiction then not x in A1 . m by A2, Th16; hence contradiction by A3, Th16; ::_thesis: verum end; suppose n < m ; ::_thesis: contradiction then not x in A1 . n by A3, Th16; hence contradiction by A2, Th16; ::_thesis: verum end; end; end; hence Partial_Diff_Union A1 is disjoint_valued by Def4; ::_thesis: verum end; end; registration let X be set ; let Si be SigmaField of X; let XSeq be SetSequence of Si; cluster Partial_Intersection XSeq -> Si -valued ; coherence Partial_Intersection XSeq is Si -valued proof defpred S1[ set ] means (Partial_Intersection XSeq) . X in Si; A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: (Partial_Intersection XSeq) . k in Si ; ::_thesis: S1[k + 1] ((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 S1[k + 1] by Def1; ::_thesis: verum end; ( XSeq . 0 in rng XSeq & (Partial_Intersection XSeq) . 0 = XSeq . 0 ) by Def1, NAT_1:51; then A3: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1); then rng (Partial_Intersection XSeq) c= Si by NAT_1:52; hence Partial_Intersection XSeq is Si -valued by RELAT_1:def_19; ::_thesis: verum end; end; registration let X be set ; let Si be SigmaField of X; let XSeq be SetSequence of Si; cluster Partial_Union XSeq -> Si -valued ; coherence Partial_Union XSeq is Si -valued proof defpred S1[ set ] means (Partial_Union XSeq) . X in Si; A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: (Partial_Union XSeq) . k in Si ; ::_thesis: S1[k + 1] ((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 S1[k + 1] by Def2; ::_thesis: verum end; ( XSeq . 0 in rng XSeq & (Partial_Union XSeq) . 0 = XSeq . 0 ) by Def2, NAT_1:51; then A3: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1); then rng (Partial_Union XSeq) c= Si by NAT_1:52; hence Partial_Union XSeq is Si -valued by RELAT_1:def_19; ::_thesis: verum end; end; registration let X be set ; let Si be SigmaField of X; let XSeq be SetSequence of Si; cluster Partial_Diff_Union XSeq -> Si -valued ; coherence Partial_Diff_Union XSeq is Si -valued 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; ::_thesis: (Partial_Diff_Union XSeq) . m in Si now__::_thesis:_(_(_m_=_0_&_(Partial_Diff_Union_XSeq)_._m_in_Si_)_or_(_ex_k_being_Nat_st_m_=_k_+_1_&_(Partial_Diff_Union_XSeq)_._m_in_Si_)_) percases ( m = 0 or ex k being Nat st m = k + 1 ) by NAT_1:6; case m = 0 ; ::_thesis: (Partial_Diff_Union XSeq) . m in Si hence (Partial_Diff_Union XSeq) . m in Si by A1; ::_thesis: verum end; case ex k being Nat st m = k + 1 ; ::_thesis: (Partial_Diff_Union XSeq) . m in Si then consider k being Nat such that A2: m = k + 1 ; reconsider k = k as Element of NAT by ORDINAL1:def_12; (XSeq . (k + 1)) \ ((Partial_Union XSeq) . k) in Si ; hence (Partial_Diff_Union XSeq) . m in Si by A2, Def3; ::_thesis: verum end; end; end; hence (Partial_Diff_Union XSeq) . m in Si ; ::_thesis: verum end; then rng (Partial_Diff_Union XSeq) c= Si by NAT_1:52; hence Partial_Diff_Union XSeq is Si -valued by RELAT_1:def_19; ::_thesis: verum end; end; theorem :: PROB_3:21 for X being set for Si being SigmaField of X for YSeq, XSeq being SetSequence of Si st YSeq = Partial_Intersection XSeq holds ( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (YSeq . n) /\ (XSeq . (n + 1)) ) ) by Def1; theorem :: PROB_3:22 for X being set for Si being SigmaField of X for YSeq, XSeq being SetSequence of Si st YSeq = Partial_Union XSeq holds ( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (YSeq . n) \/ (XSeq . (n + 1)) ) ) by Def2; theorem :: PROB_3:23 for n being Nat for X being set for Si being SigmaField of X for XSeq being SetSequence of Si holds (Partial_Intersection XSeq) . n c= XSeq . n by Th8; theorem :: PROB_3:24 for n being Nat for X being set for Si being SigmaField of X for XSeq being SetSequence of Si holds XSeq . n c= (Partial_Union XSeq) . n by Th9; theorem :: PROB_3:25 for n being Nat for X, x being set for Si being SigmaField of X for XSeq being SetSequence of Si holds ( x in (Partial_Intersection XSeq) . n iff for k being Nat st k <= n holds x in XSeq . k ) by Th12; theorem :: PROB_3:26 for n being Nat for X, x being set for Si being SigmaField of X for XSeq being SetSequence of Si holds ( x in (Partial_Union XSeq) . n iff ex k being Nat st ( k <= n & x in XSeq . k ) ) by Th13; theorem :: PROB_3:27 for X being set for Si being SigmaField of X for XSeq being SetSequence of Si holds Partial_Intersection XSeq is V70() by Th10; theorem :: PROB_3:28 for X being set for Si being SigmaField of X for XSeq being SetSequence of Si holds Partial_Union XSeq is V71() by Th11; theorem :: PROB_3:29 for X being set for Si being SigmaField of X for XSeq being SetSequence of Si holds Intersection (Partial_Intersection XSeq) = Intersection XSeq by Th14; theorem :: PROB_3:30 for X being set for Si being SigmaField of X for XSeq being SetSequence of Si holds Union (Partial_Union XSeq) = Union XSeq by Th15; theorem :: PROB_3:31 for X being set for Si being SigmaField of X for YSeq, XSeq being SetSequence of Si st YSeq = Partial_Diff_Union XSeq holds ( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (XSeq . (n + 1)) \ ((Partial_Union XSeq) . n) ) ) by Def3; theorem :: PROB_3:32 for n being Nat for X, x being set for Si being SigmaField of X for XSeq being SetSequence of Si holds ( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds not x in XSeq . k ) ) ) by Th16; theorem :: PROB_3:33 for n being Nat for X being set for Si being SigmaField of X for XSeq being SetSequence of Si holds (Partial_Diff_Union XSeq) . n c= XSeq . n by Th17; theorem :: PROB_3:34 for n being Nat for X being set for Si being SigmaField of X for XSeq being SetSequence of Si holds (Partial_Diff_Union XSeq) . n c= (Partial_Union XSeq) . n by Th18; theorem :: PROB_3:35 for X being set for Si being SigmaField of X for XSeq being SetSequence of Si holds Partial_Union (Partial_Diff_Union XSeq) = Partial_Union XSeq by Th19; theorem :: PROB_3:36 for X being set for Si being SigmaField of X for XSeq being SetSequence of Si holds Union (Partial_Diff_Union XSeq) = Union XSeq by Th20; theorem Th37: :: PROB_3:37 for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds P * (Partial_Union ASeq) is non-decreasing proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds P * (Partial_Union ASeq) is non-decreasing let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma holds P * (Partial_Union ASeq) is non-decreasing let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds P * (Partial_Union ASeq) is non-decreasing let P be Probability of Sigma; ::_thesis: P * (Partial_Union ASeq) is non-decreasing Partial_Union ASeq is V71() by Th11; hence P * (Partial_Union ASeq) is non-decreasing by Th6; ::_thesis: verum end; theorem :: PROB_3:38 for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds P * (Partial_Intersection ASeq) is non-increasing let P be Probability of Sigma; ::_thesis: P * (Partial_Intersection ASeq) is non-increasing Partial_Intersection ASeq is V70() by Th10; hence P * (Partial_Intersection ASeq) is non-increasing by Th7; ::_thesis: verum end; theorem :: PROB_3:39 for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing let P be Probability of Sigma; ::_thesis: Partial_Sums (P * ASeq) is non-decreasing for n being Element of NAT holds (P * ASeq) . n >= 0 by Th4; hence Partial_Sums (P * ASeq) is non-decreasing by SERIES_1:16; ::_thesis: verum end; theorem Th40: :: PROB_3:40 for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0 proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0 let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0 let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0 let P be Probability of Sigma; ::_thesis: (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0 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 (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0 by A2; ::_thesis: verum end; theorem Th41: :: PROB_3:41 for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds ( 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 let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds ( 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) ) let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma holds ( 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) ) let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds ( 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) ) let P be Probability of Sigma; ::_thesis: ( 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) ) A1: P * (Partial_Union ASeq) is non-decreasing by Th37; A2: Partial_Union ASeq is V71() 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 ( 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) ) by A2, A3, A1, PROB_2:10, RINFSUP1:24; ::_thesis: verum end; theorem Th42: :: PROB_3:42 for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma st ASeq is V73() holds for n, m being Nat st n < m holds (Partial_Union ASeq) . n misses ASeq . m proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma st ASeq is V73() holds for n, m being Nat st n < m holds (Partial_Union ASeq) . n misses ASeq . m let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma st ASeq is V73() holds for n, m being Nat st n < m holds (Partial_Union ASeq) . n misses ASeq . m let ASeq be SetSequence of Sigma; ::_thesis: ( ASeq is V73() implies for n, m being Nat st n < m holds (Partial_Union ASeq) . n misses ASeq . m ) assume A1: ASeq is V73() ; ::_thesis: for n, m being Nat st n < m holds (Partial_Union ASeq) . n misses ASeq . m let n, m be Nat; ::_thesis: ( n < m implies (Partial_Union ASeq) . n misses ASeq . m ) assume A2: n < m ; ::_thesis: (Partial_Union ASeq) . n misses ASeq . m assume (Partial_Union ASeq) . n meets ASeq . m ; ::_thesis: contradiction then consider x being set such that A3: x in (Partial_Union ASeq) . n and A4: x in ASeq . m by XBOOLE_0:3; consider k being Nat such that A5: k <= n and A6: x in ASeq . k by A3, Th13; ( m in NAT & k in NAT ) by ORDINAL1:def_12; then ASeq . k misses ASeq . m by A1, A2, A5, PROB_2:def_3; then (ASeq . k) /\ (ASeq . m) = {} by XBOOLE_0:def_7; hence contradiction by A4, A6, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th43: :: PROB_3:43 for n being Nat for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n proof let n be Nat; ::_thesis: for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq is V73() holds (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n let P be Probability of Sigma; ::_thesis: ( ASeq is V73() implies (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n ) A1: dom (P * ASeq) = NAT by SEQ_1:1; defpred S1[ 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 V73() ; ::_thesis: (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n A4: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: (P * (Partial_Union ASeq)) . k = (Partial_Sums (P * ASeq)) . k ; ::_thesis: S1[k + 1] k < k + 1 by NAT_1:13; then A6: (Partial_Union ASeq) . k misses ASeq . (k + 1) by A3, Th42; reconsider k = 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 S1[k + 1] by A5, A7; ::_thesis: verum end; A8: S1[ 0 ] by Th40; for k being Nat holds S1[k] from NAT_1:sch_2(A8, A4); hence (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n ; ::_thesis: verum end; theorem Th44: :: PROB_3:44 for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq is V73() holds P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) let P be Probability of Sigma; ::_thesis: ( ASeq is V73() implies P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) ) assume ASeq is V73() ; ::_thesis: P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) then for n being Element of NAT holds (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n by Th43; hence P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) by FUNCT_2:63; ::_thesis: verum end; theorem Th45: :: PROB_3:45 for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds ( 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 let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds ( 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) ) let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds ( 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) ) let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq is V73() holds ( 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) ) let P be Probability of Sigma; ::_thesis: ( ASeq is V73() 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) ) ) assume ASeq is V73() ; ::_thesis: ( 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) ) then P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) by Th44; hence ( 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) ) by Th41; ::_thesis: verum end; theorem Th46: :: PROB_3:46 for Omega being non empty set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds P . (Union ASeq) = Sum (P * ASeq) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds P . (Union ASeq) = Sum (P * ASeq) let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma st ASeq is V73() holds P . (Union ASeq) = Sum (P * ASeq) let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma st ASeq is V73() holds P . (Union ASeq) = Sum (P * ASeq) let P be Probability of Sigma; ::_thesis: ( ASeq is V73() implies P . (Union ASeq) = Sum (P * ASeq) ) assume ASeq is V73() ; ::_thesis: P . (Union ASeq) = Sum (P * ASeq) then lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) by Th45; hence P . (Union ASeq) = Sum (P * ASeq) by SERIES_1:def_3; ::_thesis: verum end; definition let X be set ; let F1 be FinSequence of bool X; let n be Nat; :: original: . redefine funcF1 . n -> Subset of X; coherence F1 . n is Subset of X proof percases ( n in dom F1 or not n in dom F1 ) ; suppose n in dom F1 ; ::_thesis: F1 . n is Subset of X hence F1 . n is Subset of X by FINSEQ_2:11; ::_thesis: verum end; suppose not n in dom F1 ; ::_thesis: F1 . n is Subset of X then F1 . n = {} by FUNCT_1:def_2; hence F1 . n is Subset of X by SUBSET_1:1; ::_thesis: verum end; end; end; end; theorem :: PROB_3:47 for X being set ex F1 being FinSequence of bool X st for k being Nat st k in dom F1 holds F1 . k = X proof let X be set ; ::_thesis: ex F1 being FinSequence of bool X st for k being Nat st k in dom F1 holds F1 . k = X now__::_thesis:_for_n_being_Element_of_NAT_ex_F1_being_FinSequence_of_bool_X_st_ for_k_being_Nat_st_k_in_dom_F1_holds_ F1_._k_=_X let n be Element of NAT ; ::_thesis: ex F1 being FinSequence of bool X st for k being Nat st k in dom F1 holds F1 . k = X set F1 = n |-> X; A1: dom (n |-> X) = Seg n by FUNCOP_1:13; rng (n |-> X) c= bool X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (n |-> X) or x in bool X ) assume x in rng (n |-> X) ; ::_thesis: x in bool X then ex i being Nat st ( i in dom (n |-> X) & (n |-> X) . i = x ) by FINSEQ_2:10; then x = X by A1, FINSEQ_2:57; hence x in bool X by ZFMISC_1:def_1; ::_thesis: verum end; then A2: n |-> X is FinSequence of bool X by FINSEQ_1:def_4; for k being Nat st k in dom (n |-> X) holds (n |-> X) . k = X by A1, FINSEQ_2:57; hence ex F1 being FinSequence of bool X st for k being Nat st k in dom F1 holds F1 . k = X by A2; ::_thesis: verum end; hence ex F1 being FinSequence of bool X st for k being Nat st k in dom F1 holds F1 . k = X ; ::_thesis: verum end; theorem :: PROB_3:48 for X being set for F1 being FinSequence of bool X holds union (rng F1) is Subset of X ; definition let X be set ; let F1 be FinSequence of bool X; :: original: Union redefine func Union F1 -> Subset of X; coherence Union F1 is Subset of X proof Union F1 = union (rng F1) by CARD_3:def_4; hence Union F1 is Subset of X ; ::_thesis: verum end; end; theorem Th49: :: PROB_3:49 for X, x being set for F1 being FinSequence of bool X holds ( x in Union F1 iff ex k being Nat st ( k in dom F1 & x in F1 . k ) ) proof let X, x be set ; ::_thesis: for F1 being FinSequence of bool X holds ( x in Union F1 iff ex k being Nat st ( k in dom F1 & x in F1 . k ) ) let F1 be FinSequence of bool X; ::_thesis: ( x in Union F1 iff ex k being Nat st ( k in dom F1 & x in F1 . k ) ) set Y = union (rng F1); A1: for x being set holds ( x in union (rng F1) iff ex k being Nat st ( k in dom F1 & x in F1 . k ) ) proof let x be set ; ::_thesis: ( x in union (rng F1) iff ex k being Nat st ( k in dom F1 & x in F1 . k ) ) thus ( x in union (rng F1) implies ex k being Nat st ( k in dom F1 & x in F1 . k ) ) ::_thesis: ( ex k being Nat st ( k in dom F1 & x in F1 . k ) implies x in union (rng F1) ) proof assume x in union (rng F1) ; ::_thesis: ex k being Nat st ( k in dom F1 & x in F1 . k ) then consider Z being set 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 ex k being Nat st ( k in dom F1 & x in F1 . k ) by A2; ::_thesis: verum end; thus ( ex k being Nat st ( k in dom F1 & x in F1 . k ) implies x in union (rng F1) ) ::_thesis: verum proof given i being Nat such that A4: i in dom F1 and A5: x in F1 . i ; ::_thesis: x in union (rng F1) F1 . i in rng F1 by A4, FUNCT_1:def_3; hence x in union (rng F1) by A5, TARSKI:def_4; ::_thesis: verum end; end; union (rng F1) = Union F1 by CARD_3:def_4; hence ( x in Union F1 iff ex k being Nat st ( k in dom F1 & x in F1 . k ) ) by A1; ::_thesis: verum end; definition let X be set ; let F1 be FinSequence of bool X; func Complement F1 -> FinSequence of bool X means :Def5: :: PROB_3:def 5 ( len it = len F1 & ( for n being Nat st n in dom it holds it . n = (F1 . n) ` ) ); existence ex b1 being FinSequence of bool X st ( len b1 = len F1 & ( for n being Nat st n in dom b1 holds b1 . n = (F1 . n) ` ) ) proof deffunc H1( Nat) -> Element of K10(X) = (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 = H1(n) ) ) from FINSEQ_2:sch_1(); take f ; ::_thesis: ( len f = len F1 & ( for n being Nat st n in dom f holds f . n = (F1 . n) ` ) ) thus ( len f = len F1 & ( for n being Nat st n in dom f holds f . n = (F1 . n) ` ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of bool X st len b1 = len F1 & ( for n being Nat st n in dom b1 holds b1 . n = (F1 . n) ` ) & len b2 = len F1 & ( for n being Nat st n in dom b2 holds b2 . n = (F1 . n) ` ) holds b1 = b2 proof let F2, F3 be FinSequence of bool X; ::_thesis: ( len F2 = len F1 & ( for n being Nat st n in dom F2 holds F2 . n = (F1 . n) ` ) & len F3 = len F1 & ( for n being Nat st n in dom F3 holds F3 . n = (F1 . n) ` ) implies F2 = F3 ) assume that A2: len F2 = len F1 and A3: for n being Nat st n in dom F2 holds F2 . n = (F1 . n) ` and A4: len F3 = len F1 and A5: for n being Nat st n in dom F3 holds F3 . n = (F1 . n) ` ; ::_thesis: F2 = F3 ( 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 ; ::_thesis: for k being Nat st k in dom F2 holds F2 . k = F3 . k let k be Nat; ::_thesis: ( k in dom F2 implies F2 . k = F3 . k ) assume A7: k in dom F2 ; ::_thesis: F2 . k = F3 . k hence F2 . k = (F1 . k) ` by A3 .= F3 . k by A5, A6, A7 ; ::_thesis: verum end; hence F2 = F3 by FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def5 defines Complement PROB_3:def_5_:_ for X being set for F1, b3 being FinSequence of bool X holds ( b3 = Complement F1 iff ( len b3 = len F1 & ( for n being Nat st n in dom b3 holds b3 . n = (F1 . n) ` ) ) ); definition let X be set ; let F1 be FinSequence of bool X; func Intersection F1 -> Subset of X equals :Def6: :: PROB_3:def 6 (Union (Complement F1)) ` if F1 <> {} otherwise {} ; coherence ( ( F1 <> {} implies (Union (Complement F1)) ` is Subset of X ) & ( not F1 <> {} implies {} is Subset of X ) ) by SUBSET_1:1; consistency for b1 being Subset of X holds verum ; end; :: deftheorem Def6 defines Intersection PROB_3:def_6_:_ for X being set for F1 being FinSequence of bool X holds ( ( F1 <> {} implies Intersection F1 = (Union (Complement F1)) ` ) & ( not F1 <> {} implies Intersection F1 = {} ) ); theorem Th50: :: PROB_3:50 for X being set for F1 being FinSequence of bool X holds dom (Complement F1) = dom F1 proof let X be set ; ::_thesis: for F1 being FinSequence of bool X holds dom (Complement F1) = dom F1 let F1 be FinSequence of bool X; ::_thesis: dom (Complement F1) = dom F1 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 ; ::_thesis: verum end; theorem Th51: :: PROB_3:51 for X, x being set for F1 being FinSequence of bool X st F1 <> {} holds ( x in Intersection F1 iff for k being Nat st k in dom F1 holds x in F1 . k ) proof let X, x be set ; ::_thesis: for F1 being FinSequence of bool X st F1 <> {} holds ( x in Intersection F1 iff for k being Nat st k in dom F1 holds x in F1 . k ) let F1 be FinSequence of bool X; ::_thesis: ( F1 <> {} implies ( x in Intersection F1 iff for k being Nat st k in dom F1 holds x in F1 . k ) ) A1: for n being Nat st n in dom F1 holds X \ ((Complement F1) . n) = F1 . n proof let n be Nat; ::_thesis: ( n in dom F1 implies X \ ((Complement F1) . n) = F1 . n ) assume n in dom F1 ; ::_thesis: X \ ((Complement F1) . n) = F1 . n 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 X \ ((Complement F1) . n) = F1 . n ; ::_thesis: verum end; assume A3: F1 <> {} ; ::_thesis: ( x in Intersection F1 iff for k being Nat st k in dom F1 holds x in F1 . k ) then A4: dom F1 <> {} by RELAT_1:41; A5: ( ( x in X & ( for n being Nat st n in dom F1 holds not x in (Complement F1) . n ) ) iff for n being Nat st n in dom F1 holds x in F1 . n ) proof hereby ::_thesis: ( ( for n being Nat st n in dom F1 holds x in F1 . n ) implies ( x in X & ( for n being Nat st n in dom F1 holds not x in (Complement F1) . n ) ) ) assume that A6: x in X and A7: for n being Nat st n in dom F1 holds not x in (Complement F1) . n ; ::_thesis: for n being Nat st n in dom F1 holds x in F1 . n let n be Nat; ::_thesis: ( n in dom F1 implies x in F1 . n ) assume A8: n in dom F1 ; ::_thesis: x in F1 . n 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; ::_thesis: verum end; assume A9: for n being Nat st n in dom F1 holds x in F1 . n ; ::_thesis: ( x in X & ( for n being Nat st n in dom F1 holds not x in (Complement F1) . n ) ) A10: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_F1_holds_ (_x_in_X_&_not_x_in_(Complement_F1)_._n_) let n be Element of NAT ; ::_thesis: ( n in dom F1 implies ( x in X & not x in (Complement F1) . n ) ) assume A11: n in dom F1 ; ::_thesis: ( x in X & not x in (Complement F1) . n ) 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; ::_thesis: verum end; ex a being set st a in dom F1 by A4, XBOOLE_0:def_1; hence ( x in X & ( for n being Nat st n in dom F1 holds not x in (Complement F1) . n ) ) by A10; ::_thesis: verum 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 being Nat 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 ( x in Intersection F1 iff for k being Nat st k in dom F1 holds x in F1 . k ) by A3, A12, A5, Def6, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th52: :: PROB_3:52 for X, x being set for F1 being FinSequence of bool X st F1 <> {} holds ( x in meet (rng F1) iff for n being Nat st n in dom F1 holds x in F1 . n ) proof let X, x be set ; ::_thesis: for F1 being FinSequence of bool X st F1 <> {} holds ( x in meet (rng F1) iff for n being Nat st n in dom F1 holds x in F1 . n ) let F1 be FinSequence of bool X; ::_thesis: ( F1 <> {} implies ( x in meet (rng F1) iff for n being Nat st n in dom F1 holds x in F1 . n ) ) assume F1 <> {} ; ::_thesis: ( x in meet (rng F1) iff for n being Nat st n in dom F1 holds x in F1 . n ) then A1: rng F1 <> {} by RELAT_1:41; A2: now__::_thesis:_for_x_being_set_st_(_for_n_being_Nat_st_n_in_dom_F1_holds_ x_in_F1_._n_)_holds_ x_in_meet_(rng_F1) let x be set ; ::_thesis: ( ( for n being Nat st n in dom F1 holds x in F1 . n ) implies x in meet (rng F1) ) assume A3: for n being Nat st n in dom F1 holds x in F1 . n ; ::_thesis: x in meet (rng F1) now__::_thesis:_for_Y_being_set_st_Y_in_rng_F1_holds_ x_in_Y let Y be set ; ::_thesis: ( Y in rng F1 implies x in Y ) assume Y in rng F1 ; ::_thesis: x in Y then consider n being set 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; ::_thesis: verum end; hence x in meet (rng F1) by A1, SETFAM_1:def_1; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_meet_(rng_F1)_holds_ for_n_being_Nat_st_n_in_dom_F1_holds_ x_in_F1_._n let x be set ; ::_thesis: ( x in meet (rng F1) implies for n being Nat st n in dom F1 holds x in F1 . n ) assume A6: x in meet (rng F1) ; ::_thesis: for n being Nat st n in dom F1 holds x in F1 . n now__::_thesis:_for_k_being_Nat_st_k_in_dom_F1_holds_ x_in_F1_._k let k be Nat; ::_thesis: ( k in dom F1 implies x in F1 . k ) assume k in dom F1 ; ::_thesis: x in F1 . k then F1 . k in rng F1 by FUNCT_1:3; hence x in F1 . k by A6, SETFAM_1:def_1; ::_thesis: verum end; hence for n being Nat st n in dom F1 holds x in F1 . n ; ::_thesis: verum end; hence ( x in meet (rng F1) iff for n being Nat st n in dom F1 holds x in F1 . n ) by A2; ::_thesis: verum end; theorem :: PROB_3:53 for X being set for F1 being FinSequence of bool X holds Intersection F1 = meet (rng F1) proof let X be set ; ::_thesis: for F1 being FinSequence of bool X holds Intersection F1 = meet (rng F1) let F1 be FinSequence of bool X; ::_thesis: Intersection F1 = meet (rng F1) percases ( F1 <> {} or F1 = {} ) ; supposeA1: F1 <> {} ; ::_thesis: Intersection F1 = meet (rng F1) now__::_thesis:_for_x_being_set_holds_ (_x_in_Intersection_F1_iff_x_in_meet_(rng_F1)_) let x be set ; ::_thesis: ( x in Intersection F1 iff x in meet (rng F1) ) ( x in Intersection F1 iff for n being Nat 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; ::_thesis: verum end; hence Intersection F1 = meet (rng F1) by TARSKI:1; ::_thesis: verum end; suppose F1 = {} ; ::_thesis: Intersection F1 = meet (rng F1) hence Intersection F1 = meet (rng F1) by Def6, RELAT_1:38, SETFAM_1:1; ::_thesis: verum end; end; end; theorem Th54: :: PROB_3:54 for X being set for F1 being FinSequence of bool X ex A1 being SetSequence of X st ( ( for k being Nat st k in dom F1 holds A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds A1 . k = {} ) ) proof let X be set ; ::_thesis: for F1 being FinSequence of bool X ex A1 being SetSequence of X st ( ( for k being Nat st k in dom F1 holds A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds A1 . k = {} ) ) deffunc H1( set ) -> set = {} ; let F1 be FinSequence of bool X; ::_thesis: ex A1 being SetSequence of X st ( ( for k being Nat st k in dom F1 holds A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds A1 . k = {} ) ) defpred S1[ set ] means $1 in dom F1; deffunc H2( set ) -> set = F1 . $1; ex f being Function st ( dom f = NAT & ( for k being set st k in NAT holds ( ( S1[k] implies f . k = H2(k) ) & ( not S1[k] implies f . k = H1(k) ) ) ) ) from PARTFUN1:sch_1(); then consider f being Function such that A1: dom f = NAT and A2: for x being set 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 being set st x in dom F1 holds F1 . x in bool X proof let x be set ; ::_thesis: ( x in dom F1 implies F1 . x in bool X ) assume x in dom F1 ; ::_thesis: F1 . x in bool X then F1 . x in rng F1 by FUNCT_1:3; hence F1 . x in bool X ; ::_thesis: verum end; for x being set st x in NAT holds f . x in bool X proof let x be set ; ::_thesis: ( x in NAT implies f . x in bool X ) assume A4: x in NAT ; ::_thesis: f . x in bool X percases ( not x in dom F1 or x in dom F1 ) ; suppose not x in dom F1 ; ::_thesis: f . x in bool X then f . x = {} by A2, A4; then f . x c= X by XBOOLE_1:2; hence f . x in bool X ; ::_thesis: verum end; supposeA5: x in dom F1 ; ::_thesis: f . x in bool X then f . x = F1 . x by A2; hence f . x in bool X by A3, A5; ::_thesis: verum end; end; end; then reconsider f = f as SetSequence of X by A1, FUNCT_2:3; take f ; ::_thesis: ( ( for k being Nat st k in dom F1 holds f . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds f . k = {} ) ) thus for k being Nat st k in dom F1 holds f . k = F1 . k by A2; ::_thesis: for k being Nat st not k in dom F1 holds f . k = {} let k be Nat; ::_thesis: ( not k in dom F1 implies f . k = {} ) k in NAT by ORDINAL1:def_12; hence ( not k in dom F1 implies f . k = {} ) by A2; ::_thesis: verum end; theorem Th55: :: PROB_3:55 for X being set for F1 being FinSequence of bool X for A1 being SetSequence of X st ( for k being Nat st k in dom F1 holds A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds A1 . k = {} ) holds ( A1 . 0 = {} & Union A1 = Union F1 ) proof let X be set ; ::_thesis: for F1 being FinSequence of bool X for A1 being SetSequence of X st ( for k being Nat st k in dom F1 holds A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds A1 . k = {} ) holds ( A1 . 0 = {} & Union A1 = Union F1 ) let F1 be FinSequence of bool X; ::_thesis: for A1 being SetSequence of X st ( for k being Nat st k in dom F1 holds A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds A1 . k = {} ) holds ( A1 . 0 = {} & Union A1 = Union F1 ) let A1 be SetSequence of X; ::_thesis: ( ( for k being Nat st k in dom F1 holds A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds A1 . k = {} ) implies ( A1 . 0 = {} & Union A1 = Union F1 ) ) assume that A1: for k being Nat st k in dom F1 holds A1 . k = F1 . k and A2: for k being Nat st not k in dom F1 holds A1 . k = {} ; ::_thesis: ( A1 . 0 = {} & Union A1 = Union F1 ) thus A1 . 0 = {} by A2, Th1; ::_thesis: Union A1 = Union F1 thus Union A1 = Union F1 ::_thesis: verum proof thus Union A1 c= Union F1 :: according to XBOOLE_0:def_10 ::_thesis: Union F1 c= Union A1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union A1 or x in Union F1 ) assume x in Union A1 ; ::_thesis: x in Union F1 then consider n being Element of 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 x in Union F1 by Th49; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union F1 or x in Union A1 ) assume x in Union F1 ; ::_thesis: x in Union A1 then consider n being Nat such that A4: ( n in dom F1 & x in F1 . n ) by Th49; ( n in NAT & x in A1 . n ) by A1, A4; hence x in Union A1 by PROB_1:12; ::_thesis: verum end; end; definition let X be set ; let Si be SigmaField of X; :: original: FinSequence redefine mode FinSequence of Si -> FinSequence of bool X; coherence for b1 being FinSequence of Si holds b1 is FinSequence of bool X proof let f be FinSequence of Si; ::_thesis: f is FinSequence of bool X thus rng f c= bool X by XBOOLE_1:1; :: according to FINSEQ_1:def_4 ::_thesis: verum end; end; definition let X be set ; let Si be SigmaField of X; let FSi be FinSequence of Si; let n be Nat; :: original: . redefine funcFSi . n -> Event of Si; coherence FSi . n is Event of Si proof percases ( n in dom FSi or not n in dom FSi ) ; suppose n in dom FSi ; ::_thesis: FSi . n is Event of Si hence FSi . n is Event of Si by FINSEQ_2:11; ::_thesis: verum end; suppose not n in dom FSi ; ::_thesis: FSi . n is Event of Si then FSi . n = {} by FUNCT_1:def_2; hence FSi . n is Event of Si by PROB_1:22; ::_thesis: verum end; end; end; end; theorem Th56: :: PROB_3:56 for X being set for Si being SigmaField of X for FSi being FinSequence of Si ex ASeq being SetSequence of Si st ( ( for k being Nat st k in dom FSi holds ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds ASeq . k = {} ) ) proof let X be set ; ::_thesis: for Si being SigmaField of X for FSi being FinSequence of Si ex ASeq being SetSequence of Si st ( ( for k being Nat st k in dom FSi holds ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds ASeq . k = {} ) ) let Si be SigmaField of X; ::_thesis: for FSi being FinSequence of Si ex ASeq being SetSequence of Si st ( ( for k being Nat st k in dom FSi holds ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds ASeq . k = {} ) ) let FSi be FinSequence of Si; ::_thesis: ex ASeq being SetSequence of Si st ( ( for k being Nat st k in dom FSi holds ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds ASeq . k = {} ) ) consider A1 being SetSequence of X such that A1: for k being Nat st k in dom FSi holds A1 . k = FSi . k and A2: for k being Nat 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; ::_thesis: A1 . n in Si percases ( not n in dom FSi or n in dom FSi ) ; suppose not n in dom FSi ; ::_thesis: A1 . n in Si then A1 . n = {} by A2; hence A1 . n in Si by PROB_1:4; ::_thesis: verum end; suppose n in dom FSi ; ::_thesis: A1 . n in Si then A1 . n = FSi . n by A1; hence A1 . n in Si ; ::_thesis: verum end; end; end; then rng A1 c= Si by NAT_1:52; then reconsider A1 = A1 as SetSequence of Si by RELAT_1:def_19; take A1 ; ::_thesis: ( ( for k being Nat st k in dom FSi holds A1 . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds A1 . k = {} ) ) thus ( ( for k being Nat st k in dom FSi holds A1 . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds A1 . k = {} ) ) by A1, A2; ::_thesis: verum end; theorem Th57: :: PROB_3:57 for X being set for Si being SigmaField of X for FSi being FinSequence of Si holds Union FSi in Si proof let X be set ; ::_thesis: for Si being SigmaField of X for FSi being FinSequence of Si holds Union FSi in Si let Si be SigmaField of X; ::_thesis: for FSi being FinSequence of Si holds Union FSi in Si let FSi be FinSequence of Si; ::_thesis: Union FSi in Si consider ASeq being SetSequence of Si such that A1: ( ( for k being Nat st k in dom FSi holds ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds ASeq . k = {} ) ) by Th56; Union ASeq = Union FSi by A1, Th55; hence Union FSi in Si by PROB_1:17; ::_thesis: verum end; registration let X be set ; let S be SigmaField of X; let F be FinSequence of S; cluster Complement F -> S -valued ; coherence Complement F is S -valued proof set G = Complement F; let x be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not x in rng (Complement F) or x in S ) assume x in rng (Complement F) ; ::_thesis: x in S then consider y being set such that A1: y in dom (Complement F) and A2: x = (Complement F) . y by FUNCT_1:def_3; reconsider y = y as Nat by A1; (Complement F) . y = (F . y) ` by A1, Def5; then (Complement F) . y is Event of S by PROB_1:20; hence x in S by A2; ::_thesis: verum end; end; theorem :: PROB_3:58 for X being set for Si being SigmaField of X for FSi being FinSequence of Si holds Intersection FSi in Si proof let X be set ; ::_thesis: for Si being SigmaField of X for FSi being FinSequence of Si holds Intersection FSi in Si let Si be SigmaField of X; ::_thesis: for FSi being FinSequence of Si holds Intersection FSi in Si let FSi be FinSequence of Si; ::_thesis: Intersection FSi in Si percases ( FSi = {} or FSi <> {} ) ; suppose FSi = {} ; ::_thesis: Intersection FSi in Si then Intersection FSi = {} by Def6; hence Intersection FSi in Si by PROB_1:4; ::_thesis: verum end; supposeA1: FSi <> {} ; ::_thesis: Intersection FSi in Si 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 Intersection FSi in Si by A2, PROB_1:def_1; ::_thesis: verum end; end; end; theorem Th59: :: PROB_3:59 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq let P be Probability of Sigma; ::_thesis: for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq let FSeq be FinSequence of Sigma; ::_thesis: dom (P * FSeq) = dom FSeq for x being set holds ( x in dom (P * FSeq) iff x in dom FSeq ) proof let x be set ; ::_thesis: ( x in dom (P * FSeq) iff x in dom FSeq ) thus ( x in dom (P * FSeq) implies x in dom FSeq ) by FUNCT_1:11; ::_thesis: ( x in dom FSeq implies x in dom (P * FSeq) ) assume A1: x in dom FSeq ; ::_thesis: x in dom (P * 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 x in dom (P * FSeq) by A1, FUNCT_1:11; ::_thesis: verum end; hence dom (P * FSeq) = dom FSeq by TARSKI:1; ::_thesis: verum end; theorem Th60: :: PROB_3:60 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL let P be Probability of Sigma; ::_thesis: for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL let FSeq be FinSequence of Sigma; ::_thesis: P * FSeq is FinSequence of REAL 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 P * FSeq is FinSequence of REAL by FINSEQ_1:def_4; ::_thesis: verum end; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let FSeq be FinSequence of Sigma; let P be Probability of Sigma; :: original: * redefine funcP * FSeq -> FinSequence of REAL ; coherence FSeq * P is FinSequence of REAL by Th60; end; theorem Th61: :: PROB_3:61 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq let P be Probability of Sigma; ::_thesis: for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq let FSeq be FinSequence of Sigma; ::_thesis: len (P * FSeq) = len FSeq dom (P * FSeq) = dom FSeq by Th59; then Seg (len (P * FSeq)) = dom FSeq by FINSEQ_1:def_3; hence len (P * FSeq) = len FSeq by FINSEQ_1:def_3; ::_thesis: verum end; theorem Th62: :: PROB_3:62 for RFin being FinSequence of REAL st len RFin = 0 holds Sum RFin = 0 proof let RFin be FinSequence of REAL ; ::_thesis: ( len RFin = 0 implies Sum RFin = 0 ) assume A1: len RFin = 0 ; ::_thesis: Sum RFin = 0 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 ; ::_thesis: verum end; theorem Th63: :: PROB_3:63 for RFin being FinSequence of REAL st len RFin >= 1 holds ex f being Real_Sequence st ( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) ) proof let RFin be FinSequence of REAL ; ::_thesis: ( len RFin >= 1 implies ex f being Real_Sequence st ( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) ) ) assume len RFin >= 1 ; ::_thesis: ex f being Real_Sequence st ( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) ) then consider f being Function of NAT,REAL such that A1: f . 1 = RFin . 1 and A2: for n being Element of 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 ; ::_thesis: ( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) ) for n being Nat st 0 <> n & n < len RFin holds f . (n + 1) = (f . n) + (RFin . (n + 1)) proof let n be Nat; ::_thesis: ( 0 <> n & n < len RFin implies f . (n + 1) = (f . n) + (RFin . (n + 1)) ) reconsider n1 = n as Element of NAT by ORDINAL1:def_12; assume that A4: 0 <> n and A5: n < len RFin ; ::_thesis: f . (n + 1) = (f . n) + (RFin . (n + 1)) thus f . (n + 1) = addreal . ((f . n1),(RFin . (n1 + 1))) by A2, A4, A5 .= (f . n) + (RFin . (n + 1)) by BINOP_2:def_9 ; ::_thesis: verum end; hence ( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) ) by A1, A3, RVSUM_1:def_12; ::_thesis: verum end; theorem Th64: :: PROB_3:64 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for FSeq being FinSequence of Sigma for ASeq being SetSequence of Sigma st ( for k being Nat st k in dom FSeq holds ASeq . k = FSeq . k ) & ( for k being Nat 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 Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for FSeq being FinSequence of Sigma for ASeq being SetSequence of Sigma st ( for k being Nat st k in dom FSeq holds ASeq . k = FSeq . k ) & ( for k being Nat 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) ) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for FSeq being FinSequence of Sigma for ASeq being SetSequence of Sigma st ( for k being Nat st k in dom FSeq holds ASeq . k = FSeq . k ) & ( for k being Nat 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) ) let P be Probability of Sigma; ::_thesis: for FSeq being FinSequence of Sigma for ASeq being SetSequence of Sigma st ( for k being Nat st k in dom FSeq holds ASeq . k = FSeq . k ) & ( for k being Nat 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) ) let FSeq be FinSequence of Sigma; ::_thesis: for ASeq being SetSequence of Sigma st ( for k being Nat st k in dom FSeq holds ASeq . k = FSeq . k ) & ( for k being Nat 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) ) let ASeq be SetSequence of Sigma; ::_thesis: ( ( for k being Nat st k in dom FSeq holds ASeq . k = FSeq . k ) & ( for k being Nat st not k in dom FSeq holds ASeq . k = {} ) implies ( 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) ) ) assume that A1: for k being Nat st k in dom FSeq holds ASeq . k = FSeq . k and A2: for k being Nat st not k in dom FSeq holds ASeq . k = {} ; ::_thesis: ( 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) ) A3: ASeq . 0 = {} by A1, A2, Th55; A4: (P * ASeq) . 0 = P . (ASeq . 0) by FUNCT_2:15 .= 0 by A3, VALUED_0:def_19 ; A5: for k being Nat st k in dom FSeq holds (P * ASeq) . k = (P * FSeq) . k proof let k be Nat; ::_thesis: ( k in dom FSeq implies (P * ASeq) . k = (P * FSeq) . k ) assume A6: k in dom FSeq ; ::_thesis: (P * ASeq) . k = (P * FSeq) . k 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 ; ::_thesis: verum 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 being Nat 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 ; ::_thesis: ( (Partial_Sums (P * ASeq)) . 1 = (P * FSeq) . 1 & ( for m being Nat st m <> 0 & m < len FSeq holds (Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1)) ) ) then 1 in dom FSeq by Th2; hence (Partial_Sums (P * ASeq)) . 1 = (P * FSeq) . 1 by A5, A7; ::_thesis: for m being Nat st m <> 0 & m < len FSeq holds (Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1)) thus for m being Nat st m <> 0 & m < len FSeq holds (Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1)) ::_thesis: verum proof let m be Nat; ::_thesis: ( m <> 0 & m < len FSeq implies (Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1)) ) assume that m <> 0 and A9: m < len FSeq ; ::_thesis: (Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1)) 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 ; ::_thesis: verum end; end; defpred S1[ 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; ::_thesis: (P * ASeq) . (((len FSeq) + 1) + m) = 0 reconsider m1 = m as Element of NAT by ORDINAL1:def_12; ((len FSeq) + 1) + m >= (len FSeq) + 1 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 ; ::_thesis: verum end; A13: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A14: (Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + k) = (Partial_Sums (P * ASeq)) . (len FSeq) ; ::_thesis: S1[k + 1] 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 S1[k + 1] by A14; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_(P_*_(Partial_Diff_Union_ASeq))_._n_<=_(P_*_ASeq)_._n let n be Element of NAT ; ::_thesis: (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n (Partial_Diff_Union ASeq) . n c= ASeq . n by Th17; hence (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n by Th5; ::_thesis: verum end; then A15: for n being Element of 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: S1[ 0 ] ; A18: for k being Nat holds S1[k] from NAT_1:sch_2(A17, A13); A19: for m being Nat st (len FSeq) + 1 <= m holds (Partial_Sums (P * ASeq)) . m = (Partial_Sums (P * ASeq)) . (len FSeq) proof let m be Nat; ::_thesis: ( (len FSeq) + 1 <= m implies (Partial_Sums (P * ASeq)) . m = (Partial_Sums (P * ASeq)) . (len FSeq) ) assume (len FSeq) + 1 <= m ; ::_thesis: (Partial_Sums (P * ASeq)) . m = (Partial_Sums (P * ASeq)) . (len FSeq) then ex k being Nat st m = ((len FSeq) + 1) + k by NAT_1:10; hence (Partial_Sums (P * ASeq)) . m = (Partial_Sums (P * ASeq)) . (len FSeq) by A18; ::_thesis: verum 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__::_thesis:_Sum_(P_*_FSeq)_=_Sum_(P_*_ASeq) percases ( len FSeq = 0 or len FSeq <> 0 ) ; suppose len FSeq = 0 ; ::_thesis: Sum (P * FSeq) = Sum (P * ASeq) then ( len (P * FSeq) = 0 & Sum (P * ASeq) = 0 ) by A4, A21, Th61, SERIES_1:def_1; hence Sum (P * FSeq) = Sum (P * ASeq) by Th62; ::_thesis: verum end; supposeA23: len FSeq <> 0 ; ::_thesis: Sum (P * FSeq) = Sum (P * ASeq) 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 being Nat 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 S2[ set , set ] means ex n being Nat 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 being Nat 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 set st x in NAT holds ex y being set st S2[x,y] proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st S2[x,y] ) assume x in NAT ; ::_thesis: ex y being set st S2[x,y] then reconsider n = x as Element of NAT ; now__::_thesis:_(_(_n_=_0_&_S2[x,_0_]_)_or_(_n_<>_0_&_n_<=_len_(P_*_FSeq)_&_S2[x,seq1_._n]_)_or_(_n_<>_0_&_not_n_<=_len_(P_*_FSeq)_&_S2[x,(Partial_Sums_(P_*_ASeq))_._(len_(P_*_FSeq))]_)_) percases ( n = 0 or ( n <> 0 & n <= len (P * FSeq) ) or ( n <> 0 & not n <= len (P * FSeq) ) ) ; case n = 0 ; ::_thesis: S2[x, 0 ] hence S2[x, 0 ] ; ::_thesis: verum end; case ( n <> 0 & n <= len (P * FSeq) ) ; ::_thesis: S2[x,seq1 . n] hence S2[x,seq1 . n] ; ::_thesis: verum end; case ( n <> 0 & not n <= len (P * FSeq) ) ; ::_thesis: S2[x,(Partial_Sums (P * ASeq)) . (len (P * FSeq))] hence S2[x,(Partial_Sums (P * ASeq)) . (len (P * FSeq))] ; ::_thesis: verum end; end; end; hence ex y being set st S2[x,y] ; ::_thesis: verum end; consider f being Function such that A29: ( dom f = NAT & ( for x being set st x in NAT holds S2[x,f . x] ) ) from CLASSES1:sch_1(A28); now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ f_._x_is_real let x be set ; ::_thesis: ( x in NAT implies f . x is real ) assume x in NAT ; ::_thesis: f . x is real then ex n being Nat 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 ; ::_thesis: verum end; then reconsider f = f as Real_Sequence by A29, SEQ_1:1; take seq = f; ::_thesis: for n being Nat 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)) ) ) let n be Nat; ::_thesis: ( ( 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)) ) ) n in NAT by ORDINAL1:def_12; then ex k being Nat 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 ( ( 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)) ) ) ; ::_thesis: verum end; then consider seq2 being Real_Sequence such that A30: for n being Nat 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 S3[ Nat] means seq2 . $1 = (Partial_Sums (P * ASeq)) . $1; A31: for k being Nat st S3[k] holds S3[k + 1] proof let k be Nat; ::_thesis: ( S3[k] implies S3[k + 1] ) assume A32: S3[k] ; ::_thesis: S3[k + 1] now__::_thesis:_(_(_k_=_0_&_seq2_._1_=_(Partial_Sums_(P_*_ASeq))_._1_)_or_(_k_<>_0_&_k_<=_(len_(P_*_FSeq))_-_1_&_seq2_._(k_+_1)_=_(Partial_Sums_(P_*_ASeq))_._(k_+_1)_)_or_(_k_<>_0_&_not_k_<=_(len_(P_*_FSeq))_-_1_&_seq2_._(k_+_1)_=_(Partial_Sums_(P_*_ASeq))_._(k_+_1)_)_) percases ( k = 0 or ( k <> 0 & k <= (len (P * FSeq)) - 1 ) or ( k <> 0 & not k <= (len (P * FSeq)) - 1 ) ) ; case k = 0 ; ::_thesis: seq2 . 1 = (Partial_Sums (P * ASeq)) . 1 thus seq2 . 1 = (Partial_Sums (P * ASeq)) . 1 by A8, A23, A24, A25, A30, NAT_1:14; ::_thesis: verum end; caseA33: ( k <> 0 & k <= (len (P * FSeq)) - 1 ) ; ::_thesis: seq2 . (k + 1) = (Partial_Sums (P * ASeq)) . (k + 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, A23, A33, A35, NAT_1:14 ; ::_thesis: verum end; case ( k <> 0 & not k <= (len (P * FSeq)) - 1 ) ; ::_thesis: seq2 . (k + 1) = (Partial_Sums (P * ASeq)) . (k + 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 ; ::_thesis: verum end; end; end; hence S3[k + 1] ; ::_thesis: verum end; seq2 . 0 = (P * ASeq) . 0 by A4, A30 .= (Partial_Sums (P * ASeq)) . 0 by SERIES_1:def_1 ; then A38: S3[ 0 ] ; A39: for k being Nat holds S3[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 ; ::_thesis: verum end; end; end; hence Sum (P * FSeq) = Sum (P * ASeq) ; ::_thesis: verum 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 ( 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) ) by A19, A20, A22, Th3, Th20, SERIES_1:def_3; ::_thesis: verum end; theorem :: PROB_3:65 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for FSeq being FinSequence of Sigma holds ( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) ) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for FSeq being FinSequence of Sigma holds ( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) ) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for FSeq being FinSequence of Sigma holds ( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) ) let P be Probability of Sigma; ::_thesis: for FSeq being FinSequence of Sigma holds ( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) ) let FSeq be FinSequence of Sigma; ::_thesis: ( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) ) consider ASeq being SetSequence of Sigma such that A1: for k being Nat st k in dom FSeq holds ASeq . k = FSeq . k and A2: for k being Nat st not k in dom FSeq holds ASeq . k = {} by Th56; P . (Union ASeq) = P . (Union FSeq) by A1, A2, Th55; then P . (Union FSeq) <= Sum (P * ASeq) by A1, A2, Th64; hence P . (Union FSeq) <= Sum (P * FSeq) by A1, A2, Th64; ::_thesis: ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) assume A3: FSeq is disjoint_valued ; ::_thesis: P . (Union FSeq) = Sum (P * FSeq) A4: ( FSeq is disjoint_valued implies ASeq is V73() ) proof assume A5: FSeq is disjoint_valued ; ::_thesis: ASeq is V73() for m, n being Element of NAT st m <> n holds ASeq . m misses ASeq . n proof let m, n be Element of NAT ; ::_thesis: ( m <> n implies ASeq . m misses ASeq . n ) assume A6: m <> n ; ::_thesis: ASeq . m misses ASeq . n percases ( ( m in dom FSeq & n in dom FSeq ) or not m in dom FSeq or not n in dom FSeq ) ; supposeA7: ( m in dom FSeq & n in dom FSeq ) ; ::_thesis: ASeq . m misses ASeq . n FSeq . m misses FSeq . n by A5, A6, PROB_2:def_2; then ASeq . m misses FSeq . n by A1, A7; hence ASeq . m misses ASeq . n by A1, A7; ::_thesis: verum end; suppose ( not m in dom FSeq or not n in dom FSeq ) ; ::_thesis: ASeq . m misses ASeq . n then ( ASeq . m = {} or ASeq . n = {} ) by A2; hence ASeq . m misses ASeq . n by XBOOLE_1:65; ::_thesis: verum end; end; end; hence ASeq is V73() by PROB_2:def_3; ::_thesis: verum end; thus P . (Union FSeq) = P . (Union ASeq) by A1, A2, Th55 .= Sum (P * ASeq) by A4, A3, Th46 .= Sum (P * FSeq) by A1, A2, Th64 ; ::_thesis: verum end; definition canceled; canceled; let X be set ; let IT be Subset-Family of X; attrIT is non-decreasing-closed means :Def9: :: PROB_3:def 9 for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds Union A1 in IT; attrIT is non-increasing-closed means :Def10: :: PROB_3:def 10 for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds Intersection A1 in IT; end; :: deftheorem PROB_3:def_7_:_ canceled; :: deftheorem PROB_3:def_8_:_ canceled; :: deftheorem Def9 defines non-decreasing-closed PROB_3:def_9_:_ for X being set for IT being Subset-Family of X holds ( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds Union A1 in IT ); :: deftheorem Def10 defines non-increasing-closed PROB_3:def_10_:_ for X being set for IT being Subset-Family of X holds ( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds Intersection A1 in IT ); theorem Th66: :: PROB_3:66 for X being set for IT being Subset-Family of X holds ( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds lim A1 in IT ) proof let X be set ; ::_thesis: for IT being Subset-Family of X holds ( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds lim A1 in IT ) let IT be Subset-Family of X; ::_thesis: ( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds lim A1 in IT ) thus ( IT is non-decreasing-closed implies for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds lim A1 in IT ) ::_thesis: ( ( for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds lim A1 in IT ) implies IT is non-decreasing-closed ) proof assume A1: IT is non-decreasing-closed ; ::_thesis: for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds lim A1 in IT now__::_thesis:_for_A1_being_SetSequence_of_X_st_A1_is_V71()_&_rng_A1_c=_IT_holds_ lim_A1_in_IT let A1 be SetSequence of X; ::_thesis: ( A1 is V71() & rng A1 c= IT implies lim A1 in IT ) assume that A2: A1 is V71() and A3: rng A1 c= IT ; ::_thesis: lim A1 in IT Union A1 in IT by A1, A2, A3, Def9; hence lim A1 in IT by A2, SETLIM_1:63; ::_thesis: verum end; hence for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds lim A1 in IT ; ::_thesis: verum end; assume A4: for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds lim A1 in IT ; ::_thesis: IT is non-decreasing-closed for A1 being SetSequence of X st A1 is V71() & rng A1 c= IT holds Union A1 in IT proof let A1 be SetSequence of X; ::_thesis: ( A1 is V71() & rng A1 c= IT implies Union A1 in IT ) assume that A5: A1 is V71() and A6: rng A1 c= IT ; ::_thesis: Union A1 in IT lim A1 in IT by A4, A5, A6; hence Union A1 in IT by A5, SETLIM_1:63; ::_thesis: verum end; hence IT is non-decreasing-closed by Def9; ::_thesis: verum end; theorem Th67: :: PROB_3:67 for X being set for IT being Subset-Family of X holds ( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds lim A1 in IT ) proof let X be set ; ::_thesis: for IT being Subset-Family of X holds ( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds lim A1 in IT ) let IT be Subset-Family of X; ::_thesis: ( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds lim A1 in IT ) thus ( IT is non-increasing-closed implies for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds lim A1 in IT ) ::_thesis: ( ( for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds lim A1 in IT ) implies IT is non-increasing-closed ) proof assume A1: IT is non-increasing-closed ; ::_thesis: for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds lim A1 in IT now__::_thesis:_for_A1_being_SetSequence_of_X_st_A1_is_V70()_&_rng_A1_c=_IT_holds_ lim_A1_in_IT let A1 be SetSequence of X; ::_thesis: ( A1 is V70() & rng A1 c= IT implies lim A1 in IT ) assume that A2: A1 is V70() and A3: rng A1 c= IT ; ::_thesis: lim A1 in IT Intersection A1 in IT by A1, A2, A3, Def10; hence lim A1 in IT by A2, SETLIM_1:64; ::_thesis: verum end; hence for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds lim A1 in IT ; ::_thesis: verum end; assume A4: for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds lim A1 in IT ; ::_thesis: IT is non-increasing-closed for A1 being SetSequence of X st A1 is V70() & rng A1 c= IT holds Intersection A1 in IT proof let A1 be SetSequence of X; ::_thesis: ( A1 is V70() & rng A1 c= IT implies Intersection A1 in IT ) assume that A5: A1 is V70() and A6: rng A1 c= IT ; ::_thesis: Intersection A1 in IT lim A1 in IT by A4, A5, A6; hence Intersection A1 in IT by A5, SETLIM_1:64; ::_thesis: verum end; hence IT is non-increasing-closed by Def10; ::_thesis: verum end; theorem Th68: :: PROB_3:68 for X being set holds ( bool X is non-decreasing-closed & bool X is non-increasing-closed ) proof let X be set ; ::_thesis: ( bool X is non-decreasing-closed & bool X is non-increasing-closed ) for A1 being SetSequence of X st A1 is V71() & rng A1 c= bool X holds Union A1 in bool X ; hence bool X is non-decreasing-closed by Def9; ::_thesis: bool X is non-increasing-closed for A1 being SetSequence of X st A1 is V70() & rng A1 c= bool X holds Intersection A1 in bool X ; hence bool X is non-increasing-closed by Def10; ::_thesis: verum end; registration let X be set ; cluster non-decreasing-closed non-increasing-closed for Element of K10(K10(X)); existence ex b1 being Subset-Family of X st ( b1 is non-decreasing-closed & b1 is non-increasing-closed ) proof take bool X ; ::_thesis: ( bool X is non-decreasing-closed & bool X is non-increasing-closed ) thus ( bool X is non-decreasing-closed & bool X is non-increasing-closed ) by Th68; ::_thesis: verum end; end; definition let X be set ; mode MonotoneClass of X is non-decreasing-closed non-increasing-closed Subset-Family of X; end; theorem Th69: :: PROB_3:69 for Z, X being set holds ( 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 let Z, X be set ; ::_thesis: ( 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 ) ) ) 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 ) ) ) ::_thesis: ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds lim A1 in Z ) implies Z is MonotoneClass of X ) proof assume A1: Z is MonotoneClass of X ; ::_thesis: ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds lim A1 in Z ) ) then reconsider Z = 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; ::_thesis: ( A1 is monotone & rng A1 c= Z implies lim A1 in Z ) assume that A2: A1 is monotone and A3: rng A1 c= Z ; ::_thesis: lim A1 in Z percases ( not A1 is V71() or not A1 is V70() ) by A2, SETLIM_1:def_1; suppose A1 is V71() ; ::_thesis: lim A1 in Z hence lim A1 in Z by A1, A3, Th66; ::_thesis: verum end; suppose A1 is V70() ; ::_thesis: lim A1 in Z hence lim A1 in Z by A1, A3, Th67; ::_thesis: verum end; end; end; hence ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds lim A1 in Z ) ) ; ::_thesis: verum 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 ; ::_thesis: Z is MonotoneClass of X reconsider Z = Z as Subset-Family of X by A4; A6: for A1 being SetSequence of X st A1 is V70() & rng A1 c= Z holds lim A1 in Z proof let A1 be SetSequence of X; ::_thesis: ( A1 is V70() & rng A1 c= Z implies lim A1 in Z ) assume A7: ( A1 is V70() & rng A1 c= Z ) ; ::_thesis: lim A1 in Z ( A1 is monotone & rng A1 c= Z implies lim A1 in Z ) by A5; hence lim A1 in Z by A7, SETLIM_1:def_1; ::_thesis: verum end; for A1 being SetSequence of X st A1 is V71() & rng A1 c= Z holds lim A1 in Z proof let A1 be SetSequence of X; ::_thesis: ( A1 is V71() & rng A1 c= Z implies lim A1 in Z ) assume A8: ( A1 is V71() & rng A1 c= Z ) ; ::_thesis: lim A1 in Z ( A1 is monotone & rng A1 c= Z implies lim A1 in Z ) by A5; hence lim A1 in Z by A8, SETLIM_1:def_1; ::_thesis: verum end; hence Z is MonotoneClass of X by A6, Th66, Th67; ::_thesis: verum end; theorem Th70: :: PROB_3:70 for X being set for F being Field_Subset of X holds ( F is SigmaField of X iff F is MonotoneClass of X ) proof let X be set ; ::_thesis: for F being Field_Subset of X holds ( F is SigmaField of X iff F is MonotoneClass of X ) let F be Field_Subset of X; ::_thesis: ( F is SigmaField of X iff F is MonotoneClass of X ) thus ( F is SigmaField of X implies F is MonotoneClass of X ) ::_thesis: ( F is MonotoneClass of X implies F is SigmaField of X ) proof assume F is SigmaField of X ; ::_thesis: F is MonotoneClass of X then reconsider F = F as SigmaField of X ; A1: for A1 being SetSequence of X st A1 is V71() & rng A1 c= F holds Union A1 in F proof let A1 be SetSequence of X; ::_thesis: ( A1 is V71() & rng A1 c= F implies Union A1 in F ) assume that A1 is V71() and A2: rng A1 c= F ; ::_thesis: Union A1 in F reconsider A2 = A1 as SetSequence of F by A2, RELAT_1:def_19; Union A2 in F by PROB_1:17; hence Union A1 in F ; ::_thesis: verum end; F is non-increasing-closed proof let A1 be SetSequence of X; :: according to PROB_3:def_10 ::_thesis: ( A1 is V70() & rng A1 c= F implies Intersection A1 in F ) assume A1 is V70() ; ::_thesis: ( not rng A1 c= F or Intersection A1 in F ) assume rng A1 c= F ; ::_thesis: Intersection A1 in F hence Intersection A1 in F by PROB_1:def_6; ::_thesis: verum end; hence F is MonotoneClass of X by A1, Def9; ::_thesis: verum end; assume A3: F is MonotoneClass of X ; ::_thesis: F is SigmaField of X for A1 being SetSequence of X st rng A1 c= F holds Intersection A1 in F proof let A1 be SetSequence of X; ::_thesis: ( rng A1 c= F implies Intersection A1 in F ) assume A4: rng A1 c= F ; ::_thesis: Intersection A1 in F set A2 = Partial_Intersection A1; defpred S1[ Nat] means (Partial_Intersection A1) . $1 in F; A5: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: (Partial_Intersection A1) . k in F ; ::_thesis: S1[k + 1] ( A1 . (k + 1) in rng A1 & (Partial_Intersection A1) . (k + 1) = ((Partial_Intersection A1) . k) /\ (A1 . (k + 1)) ) by Def1, NAT_1:51; hence (Partial_Intersection A1) . (k + 1) in F by A4, A6, FINSUB_1:def_2; ::_thesis: verum end; ( A1 . 0 in rng A1 & (Partial_Intersection A1) . 0 = A1 . 0 ) by Def1, NAT_1:51; then A7: S1[ 0 ] by A4; for k being Nat holds S1[k] from NAT_1:sch_2(A7, A5); then A8: rng (Partial_Intersection A1) c= F by NAT_1:52; Partial_Intersection A1 is V70() by Th10; then Intersection (Partial_Intersection A1) in F by A3, A8, Def10; hence Intersection A1 in F by Th14; ::_thesis: verum end; hence F is SigmaField of X by PROB_1:def_6; ::_thesis: verum end; theorem :: PROB_3:71 for Omega being non empty set holds bool Omega is MonotoneClass of Omega by Th68; definition let Omega be non empty set ; let X be Subset-Family of Omega; func monotoneclass X -> MonotoneClass of Omega means :Def11: :: PROB_3:def 11 ( X c= it & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds it c= Z ) ); existence ex b1 being MonotoneClass of Omega st ( X c= b1 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds b1 c= Z ) ) proof set V = { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; set Y = meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; A1: for Z being set st Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } holds X c= Z proof let Z be set ; ::_thesis: ( Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } implies X c= Z ) assume Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; ::_thesis: X c= Z then ex M being Subset-Family of Omega st ( Z = M & X c= M & M is MonotoneClass of Omega ) ; hence X c= Z ; ::_thesis: verum end; bool Omega is MonotoneClass of Omega by Th68; then A2: bool Omega in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; for MSeq being SetSequence of Omega st MSeq is monotone & rng MSeq c= meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } holds lim MSeq in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } proof let MSeq be SetSequence of Omega; ::_thesis: ( MSeq is monotone & rng MSeq c= meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } implies lim MSeq in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ) assume that A3: MSeq is monotone and A4: rng MSeq c= meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; ::_thesis: lim MSeq in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } now__::_thesis:_for_Z_being_set_st_Z_in__{__M_where_M_is_Subset-Family_of_Omega_:_(_X_c=_M_&_M_is_MonotoneClass_of_Omega_)__}__holds_ lim_MSeq_in_Z let Z be set ; ::_thesis: ( Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } implies lim MSeq in Z ) assume A5: Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; ::_thesis: lim MSeq in Z now__::_thesis:_for_n_being_Nat_holds_MSeq_._n_in_Z let n be Nat; ::_thesis: MSeq . n in Z MSeq . n in rng MSeq by NAT_1:51; hence MSeq . n in Z by A4, A5, SETFAM_1:def_1; ::_thesis: verum 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; ::_thesis: verum end; hence lim MSeq in meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } by A2, SETFAM_1:def_1; ::_thesis: verum end; then reconsider Y = meet { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } as MonotoneClass of Omega by A2, Th69, SETFAM_1:3; take Y ; ::_thesis: ( X c= Y & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds Y c= Z ) ) for Z being set st X c= Z & Z is MonotoneClass of Omega holds Y c= Z proof let Z be set ; ::_thesis: ( X c= Z & Z is MonotoneClass of Omega implies Y c= Z ) assume ( X c= Z & Z is MonotoneClass of Omega ) ; ::_thesis: Y c= Z then Z in { M where M is Subset-Family of Omega : ( X c= M & M is MonotoneClass of Omega ) } ; hence Y c= Z by SETFAM_1:3; ::_thesis: verum end; hence ( X c= Y & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds Y c= Z ) ) by A2, A1, SETFAM_1:5; ::_thesis: verum end; uniqueness for b1, b2 being MonotoneClass of Omega st X c= b1 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds b1 c= Z ) & X c= b2 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds b2 c= Z ) holds b1 = b2 proof let R1, R2 be MonotoneClass of Omega; ::_thesis: ( X c= R1 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds R1 c= Z ) & X c= R2 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds R2 c= Z ) implies R1 = R2 ) assume that A7: X c= R1 and A8: ( ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds R1 c= Z ) & X c= R2 ) and A9: for Z being set st X c= Z & Z is MonotoneClass of Omega holds R2 c= Z ; ::_thesis: R1 = R2 thus R1 c= R2 by A8; :: according to XBOOLE_0:def_10 ::_thesis: R2 c= R1 thus R2 c= R1 by A7, A9; ::_thesis: verum end; end; :: deftheorem Def11 defines monotoneclass PROB_3:def_11_:_ for Omega being non empty set for X being Subset-Family of Omega for b3 being MonotoneClass of Omega holds ( b3 = monotoneclass X iff ( X c= b3 & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds b3 c= Z ) ) ); theorem Th72: :: PROB_3:72 for Omega being non empty set for Z being Field_Subset of Omega holds monotoneclass Z is Field_Subset of Omega proof let Omega be non empty set ; ::_thesis: for Z being Field_Subset of Omega holds monotoneclass Z is Field_Subset of Omega let Z be Field_Subset of Omega; ::_thesis: monotoneclass Z is Field_Subset of Omega A1: Z c= monotoneclass Z by Def11; 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 ) } holds 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 ; ::_thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies for z being set st z in Y holds ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) ) assume A3: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; ::_thesis: for z being set st z in Y holds ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ 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 ) ::_thesis: verum proof let z be set ; ::_thesis: ( z in Y implies ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) ) assume z in Y ; ::_thesis: ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) then ex z1 being Element of Z1 st ( z = z1 & y \ z1 in Z1 & z1 \ y in Z1 & z1 /\ y in Z1 ) by A3; hence ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) ; ::_thesis: verum end; end; A4: for y being Element of Z1 for Y being set 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; ::_thesis: for Y being set 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 let Y be set ; ::_thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Y is MonotoneClass of Omega ) assume A5: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; ::_thesis: Y is MonotoneClass of Omega 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; ::_thesis: ( A1 is monotone & rng A1 c= Y implies lim A1 in Y ) assume that A7: A1 is monotone and A8: rng A1 c= Y ; ::_thesis: lim A1 in Y A9: A1 is convergent by A7, SETLIM_1:65; for n being Nat holds A1 . n in Z1 proof let n be Nat; ::_thesis: A1 . n in Z1 A1 . n in rng A1 by NAT_1:51; hence A1 . n in Z1 by A2, A5, A8; ::_thesis: verum end; then rng A1 c= Z1 by NAT_1:52; then A10: lim A1 is Element of Z1 by A7, Th69; for n being Nat holds (A1 (\) y) . n in Z1 proof let n be Nat; ::_thesis: (A1 (\) y) . n in Z1 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 (A1 (\) y) . n in Z1 by SETLIM_2:def_8; ::_thesis: verum end; then A11: rng (A1 (\) y) c= Z1 by NAT_1:52; for n being Nat holds (y (/\) A1) . n in Z1 proof let n be Nat; ::_thesis: (y (/\) A1) . n in Z1 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 (y (/\) A1) . n in Z1 by SETLIM_2:def_5; ::_thesis: verum 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 being Nat holds (y (\) A1) . n in Z1 proof let n be Nat; ::_thesis: (y (\) A1) . n in Z1 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 (y (\) A1) . n in Z1 by SETLIM_2:def_7; ::_thesis: verum 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 lim A1 in Y by A5, A10, A15, A13; ::_thesis: verum end; for z being set st z in Y holds z in Z1 by A2, A5; then Y c= Z1 by TARSKI:def_3; hence Y is MonotoneClass of Omega by A6, Th69, XBOOLE_1:1; ::_thesis: verum end; A16: for y being Element of Z for Y being set 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; ::_thesis: for Y being set 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 let Y be set ; ::_thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Z1 c= Y ) assume A17: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; ::_thesis: Z1 c= Y A18: Z c= Y proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in Y ) assume A19: z in Z ; ::_thesis: z in Y then A20: z /\ y in Z by FINSUB_1:def_2; ( z \ y in Z & y \ z in Z ) by A19, PROB_1:6; hence z in Y by A1, A17, A19, A20; ::_thesis: verum end; y in Z ; then Y is MonotoneClass of Omega by A1, A4, A17; hence Z1 c= Y by A18, Def11; ::_thesis: verum end; A21: for y being Element of Z1 for Y being set 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; ::_thesis: for Y being set 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 let Y be set ; ::_thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Z1 c= Y ) assume A22: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; ::_thesis: Z1 c= Y A23: Z c= Y proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in Y ) set Y1 = { x where x is Element of Z1 : ( z \ x in Z1 & x \ z in Z1 & x /\ z in Z1 ) } ; assume A24: z in Z ; ::_thesis: z in Y then A25: Z1 c= { x where x is Element of Z1 : ( z \ x in Z1 & x \ z in Z1 & x /\ z in Z1 ) } by A16; A26: y in Z1 ; then A27: z /\ y in Z1 by A2, A25; ( z \ y in Z1 & y \ z in Z1 ) by A2, A25, A26; hence z in Y by A1, A22, A24, A27; ::_thesis: verum end; Y is MonotoneClass of Omega by A4, A22; hence Z1 c= Y by A23, Def11; ::_thesis: verum 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; ::_thesis: ( y in Z1 implies y ` in Z1 ) assume A30: y in Z1 ; ::_thesis: 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= { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } by A21, A30; then Omega \ y in Z1 by A2, A29; hence y ` in Z1 by SUBSET_1:def_4; ::_thesis: verum end; now__::_thesis:_for_y,_z_being_set_st_y_in_Z1_&_z_in_Z1_holds_ y_/\_z_in_Z1 let y, z be set ; ::_thesis: ( y in Z1 & z in Z1 implies y /\ z in Z1 ) assume that A31: y in Z1 and A32: z in Z1 ; ::_thesis: y /\ 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= { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } by A21, A31; hence y /\ z in Z1 by A2, A32; ::_thesis: verum end; hence monotoneclass Z is Field_Subset of Omega by A28, FINSUB_1:def_2, PROB_1:def_1; ::_thesis: verum end; theorem :: PROB_3:73 for Omega being non empty set for Z being Field_Subset of Omega holds sigma Z = monotoneclass Z proof let Omega be non empty set ; ::_thesis: for Z being Field_Subset of Omega holds sigma Z = monotoneclass Z let Z be Field_Subset of Omega; ::_thesis: sigma Z = monotoneclass Z monotoneclass Z is Field_Subset of Omega by Th72; then A1: monotoneclass Z is SigmaField of Omega by Th70; Z c= monotoneclass Z by Def11; hence sigma Z c= monotoneclass Z by A1, PROB_1:def_9; :: according to XBOOLE_0:def_10 ::_thesis: monotoneclass Z c= sigma Z ( sigma Z is MonotoneClass of Omega & Z c= sigma Z ) by Th70, PROB_1:def_9; hence monotoneclass Z c= sigma Z by Def11; ::_thesis: verum end;