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, Th60;
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 S₁[ 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 S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A14: (Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + k) = (Partial_Sums (P * ASeq)) . (len FSeq) ; :: thesis: S₁[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 S₁[k + 1] by A14; :: thesis: verum

end;

now

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 Th20;
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;
A17: Partial_Sums (P * (Partial_Diff_Union ASeq)) is convergent by Th50;
(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 A18: S₁[ 0 ] ;
A19: for k being Nat holds S₁[k] from NAT_1:sch 2(A18, A13);
A20: 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 A19; :: thesis: verum

end;

then A21: lim (Partial_Sums (P * ASeq)) = (Partial_Sums (P * ASeq)) . (len FSeq) by Th3;
then A22: Sum (P * ASeq) = (Partial_Sums (P * ASeq)) . (len FSeq) by SERIES_1:def 3;
A23: Sum (P * FSeq) = Sum (P * ASeq)

proof

now

per cases ( 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, A22, Th66, SERIES_1:def 1;
hence Sum (P * FSeq) = Sum (P * ASeq) by Th67; :: thesis: verum

end;

suppose A24: len FSeq <> 0 ; :: thesis: Sum (P * FSeq) = Sum (P * ASeq)

then 1 <= len FSeq by NAT_1:14;
then A25: 1 <= len (P * FSeq) by Th66;
then consider seq1 being Real_Sequence such that
A26: seq1 . 1 = (P * FSeq) . 1 and
A27: for n being Nat st 0 <> n & n < len (P * FSeq) holds
seq1 . (n + 1) = (seq1 . n) + ((P * FSeq) . (n + 1)) and
A28: Sum (P * FSeq) = seq1 . (len (P * FSeq)) by Th68;
defpred S₂[ 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

A29: for x being set st x in NAT holds
ex y being set st S₂[x,y]

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st S₂[x,y] )
assume x in NAT ; :: thesis: ex y being set st S₂[x,y]
then reconsider n = x as Element of NAT ;

now

per cases ( n = 0 or ( n <> 0 & n <= len (P * FSeq) ) or ( n <> 0 & not n <= len (P * FSeq) ) ) ;

case n = 0 ; :: thesis: S₂[x, 0 ]

hence S₂[x, 0 ] ; :: thesis: verum

end;

case ( n <> 0 & n <= len (P * FSeq) ) ; :: thesis: S₂[x,seq1 . n]

hence S₂[x,seq1 . n] ; :: thesis: verum

end;

case ( n <> 0 & not n <= len (P * FSeq) ) ; :: thesis: S₂[x,(Partial_Sums (P * ASeq)) . (len (P * FSeq))]

hence S₂[x,(Partial_Sums (P * ASeq)) . (len (P * FSeq))] ; :: thesis: verum

end;

end;

end;

hence ex y being set st S₂[x,y] ; :: thesis: verum

end;

consider f being Function such that
A30: ( dom f = NAT & ( for x being set st x in NAT holds
S₂[x,f . x] ) ) from CLASSES1:sch 1(A29);

now

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 A30;
hence f . x is real ; :: thesis: verum

end;

then reconsider f = f as Real_Sequence by A30, 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 A30;
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
A31: 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 S₃[ Nat] means seq2 . $1 = (Partial_Sums (P * ASeq)) . $1;
A32: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis: ( S₃[k] implies S₃[k + 1] )
assume A33: S₃[k] ; :: thesis: S₃[k + 1]

now

per cases ( 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, A24, A25, A26, A31, NAT_1:14; :: thesis: verum

end;

case A34: ( k <> 0 & k <= (len (P * FSeq)) - 1 ) ; :: thesis: seq2 . (k + 1) = (Partial_Sums (P * ASeq)) . (k + 1)

then A35: k + 0 < ((len (P * FSeq)) - 1) + 1 by XREAL_1:8;
then A36: k < len FSeq by Th66;
k + 1 <= ((len (P * FSeq)) - 1) + 1 by A34, XREAL_1:7;
hence seq2 . (k + 1) = seq1 . (k + 1) by A31
.= (seq1 . k) + ((P * FSeq) . (k + 1)) by A27, A34, A35
.= ((Partial_Sums (P * ASeq)) . k) + ((P * FSeq) . (k + 1)) by A31, A33, A34, A35
.= (Partial_Sums (P * ASeq)) . (k + 1) by A8, A24, A34, A36, 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 A37: 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
A38: k + 1 = ((len (P * FSeq)) + 1) + i by NAT_1:10;
thus seq2 . (k + 1) = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) by A31, A37
.= (Partial_Sums (P * ASeq)) . (len FSeq) by Th66
.= (Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + i) by A19
.= (Partial_Sums (P * ASeq)) . (k + 1) by A38, Th66 ; :: thesis: verum

end;

end;

end;

hence S₃[k + 1] ; :: thesis: verum

end;

seq2 . 0 = (P * ASeq) . 0 by A4, A31
.= (Partial_Sums (P * ASeq)) . 0 by SERIES_1:def 1 ;
then A39: S₃[ 0 ] ;
A40: for k being Nat holds S₃[k] from NAT_1:sch 2(A39, A32);
len (P * FSeq) <> 0 by A24, Th66;
then seq2 . (len (P * FSeq)) = Sum (P * FSeq) by A28, A31;
hence Sum (P * FSeq) = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) by A40
.= Sum (P * ASeq) by A22, Th66 ;
:: thesis: verum

end;

end;

end;

hence Sum (P * FSeq) = Sum (P * ASeq) ; :: thesis: verum

end;

Partial_Sums (P * ASeq) is convergent by A20, Th3;
then lim (Partial_Sums (P * (Partial_Diff_Union ASeq))) <= lim (Partial_Sums (P * ASeq)) by A17, 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 Th51;
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 A20, A21, A23, Th3, Th23, SERIES_1:def 3; :: thesis: verum