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 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 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 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 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 ; :: 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 A1: ( ( 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 = {} ) ) ; :: 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) )
A2: ASeq . 0 = {} by A1, Th60;
A3: ( (P * ASeq) . 0 = 0 & ( for m being Nat holds (P * ASeq) . (((len FSeq) + 1) + m) = 0 ) )

proof

thus (P * ASeq) . 0 = P . (ASeq . 0 ) by FUNCT_2:21
.= 0 by A2, VALUED_0:def 19 ; :: thesis: for m being Nat holds (P * ASeq) . (((len FSeq) + 1) + m) = 0
thus for m being Nat holds (P * ASeq) . (((len FSeq) + 1) + m) = 0 :: thesis: verum

proof

let m be Nat; :: thesis: (P * ASeq) . (((len FSeq) + 1) + m) = 0
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;
set k = (len FSeq) + 1;
((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:27;
then A4: ASeq . (((len FSeq) + 1) + m) = {} by A1;
thus (P * ASeq) . (((len FSeq) + 1) + m) = P . (ASeq . (((len FSeq) + 1) + m1)) by FUNCT_2:21
.= 0 by A4, VALUED_0:def 19 ; :: thesis: verum

end;

end;

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 13;
hence (P * ASeq) . k = P . (ASeq . k) by FUNCT_2:21
.= P . (FSeq . k) by A1, A6
.= (P * FSeq) . k by A6, FUNCT_1:23 ;
:: 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 A3 ;
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 ( m <> 0 & m < len FSeq ) ; :: thesis: (Partial_Sums (P * ASeq)) . (m + 1) = ((Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1))
then m + 1 in Seg (len FSeq) by FINSEQ_3:12;
then A9: m + 1 in dom FSeq by FINSEQ_1:def 3;
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;
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, A9 ; :: thesis: verum

end;

end;

defpred S₁[ Nat] means (Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + $1) = (Partial_Sums (P * ASeq)) . (len FSeq);
(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 A3 ;
then A10: S₁[ 0 ] ;
A11: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A12: (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 13;
(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 A3 ;
hence S₁[k + 1] by A12; :: thesis: verum

end;

A13: for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A11);
A14: ( Partial_Sums (P * ASeq) is convergent & Sum (P * ASeq) = (Partial_Sums (P * ASeq)) . (len FSeq) )

proof

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 A15: (len FSeq) + 1 <= m ; :: thesis: (Partial_Sums (P * ASeq)) . m = (Partial_Sums (P * ASeq)) . (len FSeq)
consider k being Nat such that
A16: m = ((len FSeq) + 1) + k by A15, NAT_1:10;
thus (Partial_Sums (P * ASeq)) . m = (Partial_Sums (P * ASeq)) . (len FSeq) by A13, A16; :: thesis: verum

end;

then ( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = (Partial_Sums (P * ASeq)) . (len FSeq) ) by Th3;
hence ( Partial_Sums (P * ASeq) is convergent & Sum (P * ASeq) = (Partial_Sums (P * ASeq)) . (len FSeq) ) by SERIES_1:def 3; :: thesis: verum

end;

A17: Sum (P * FSeq) = Sum (P * ASeq)

proof

now

per cases ( len FSeq = 0 or len FSeq <> 0 ) ;

suppose A18: len FSeq = 0 ; :: thesis: Sum (P * FSeq) = Sum (P * ASeq)

then A19: len (P * FSeq) = 0 by Th66;
Sum (P * ASeq) = 0 by A3, A14, A18, SERIES_1:def 1;
hence Sum (P * FSeq) = Sum (P * ASeq) by A19, Th67; :: thesis: verum

end;

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

then A21: len (P * FSeq) <> 0 by Th66;
1 <= len FSeq by A20, NAT_1:14;
then A22: 1 <= len (P * FSeq) by Th66;
then consider seq1 being Real_Sequence such that
A23: ( seq1 . 1 = (P * FSeq) . 1 & ( for n being Nat st 0 <> n & n < len (P * FSeq) holds
seq1 . (n + 1) = (seq1 . n) + ((P * FSeq) . (n + 1)) ) & 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

A24: 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
A26: ( dom f = NAT & ( for x being set st x in NAT holds
S₂[x,f . x] ) ) from CLASSES1:sch 1(A24);

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

end;

then reconsider f = f as Real_Sequence by A26, SEQ_1:3;
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 13;
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 A26;
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
A27: 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)) ) ) ;
A28: seq2 . (len (P * FSeq)) = Sum (P * FSeq) by A21, A23, A27;
defpred S₃[ Nat] means seq2 . $1 = (Partial_Sums (P * ASeq)) . $1;
seq2 . 0 = (P * ASeq) . 0 by A3, A27
.= (Partial_Sums (P * ASeq)) . 0 by SERIES_1:def 1 ;
then A29: S₃[ 0 ] ;
A30: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis: ( S₃[k] implies S₃[k + 1] )
assume A31: 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, A20, A22, A23, A27, NAT_1:14; :: thesis: verum

end;

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

then A33: k + 0 < ((len (P * FSeq)) - 1) + 1 by XREAL_1:10;
then A34: k < len FSeq by Th66;
k + 1 <= ((len (P * FSeq)) - 1) + 1 by A32, XREAL_1:9;
hence seq2 . (k + 1) = seq1 . (k + 1) by A27
.= (seq1 . k) + ((P * FSeq) . (k + 1)) by A23, A32, A33
.= ((Partial_Sums (P * ASeq)) . k) + ((P * FSeq) . (k + 1)) by A27, A31, A32, A33
.= (Partial_Sums (P * ASeq)) . (k + 1) by A8, A20, A32, A34, 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 A35: ( k + 1 <> 0 & k + 1 > ((len (P * FSeq)) - 1) + 1 ) by XREAL_1:10;
then k + 1 >= (len (P * FSeq)) + 1 by NAT_1:13;
then consider i being Nat such that
A36: k + 1 = ((len (P * FSeq)) + 1) + i by NAT_1:10;
thus seq2 . (k + 1) = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) by A27, A35
.= (Partial_Sums (P * ASeq)) . (len FSeq) by Th66
.= (Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + i) by A13
.= (Partial_Sums (P * ASeq)) . (k + 1) by A36, Th66 ; :: thesis: verum

end;

end;

end;

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

end;

for k being Nat holds S₃[k] from NAT_1:sch 2(A29, A30);
hence Sum (P * FSeq) = (Partial_Sums (P * ASeq)) . (len (P * FSeq)) by A28
.= Sum (P * ASeq) by A14, Th66 ;
:: thesis: verum

end;

end;

end;

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

end;

A37: @Partial_Diff_Union ASeq is disjoint_valued by Th24;
then A38: Partial_Sums (P * (@Partial_Diff_Union ASeq)) is convergent by Th50;

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 for n being Element of NAT holds (Partial_Sums (P * (@Partial_Diff_Union ASeq))) . n <= (Partial_Sums (P * ASeq)) . n by SERIES_1:17;
then lim (Partial_Sums (P * (@Partial_Diff_Union ASeq))) <= lim (Partial_Sums (P * ASeq)) by A14, A38, SEQ_2:32;
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 A37, 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 A14, A17, Th23; :: thesis: verum