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) )

reconsider XSeq = ASeq as SetSequence of Omega ;

( ( for k being Nat st k in dom FSeq holds

XSeq . k = FSeq . k ) & ( for k being Nat st not k in dom FSeq holds

XSeq . k = {} ) ) by A1, A2;

then A3: ASeq . 0 = {} by Th55;

A4: (P * ASeq) . 0 = P . (ASeq . 0) by FUNCT_2:15

.= 0 by A3, VALUED_0:def 19 ;

A5: for k being Nat st k in dom FSeq holds

(P * ASeq) . k = (P * FSeq) . k

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)) ) ) )_{1}[ 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_{1}[k] holds

S_{1}[k + 1]

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: S_{1}[ 0 ]
;

A18: for k being Nat holds S_{1}[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)

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

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

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

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) )

reconsider XSeq = ASeq as SetSequence of Omega ;

( ( for k being Nat st k in dom FSeq holds

XSeq . k = FSeq . k ) & ( for k being Nat st not k in dom FSeq holds

XSeq . k = {} ) ) by A1, A2;

then A3: ASeq . 0 = {} by Th55;

A4: (P * ASeq) . 0 = P . (ASeq . 0) by FUNCT_2:15

.= 0 by A3, VALUED_0:def 19 ;

A5: for k being Nat st k in dom FSeq holds

(P * ASeq) . k = (P * FSeq) . k

proof

1 = 0 + 1
;
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;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

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

defpred S
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

end;(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;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

A11: for m being Nat holds (P * ASeq) . (((len FSeq) + 1) + m) = 0

proof

A13:
for k being Nat st S
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;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

S

proof

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A14: (Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + k) = (Partial_Sums (P * ASeq)) . (len FSeq) ; :: thesis: S_{1}[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_{1}[k + 1]
by A14; :: thesis: verum

end;assume A14: (Partial_Sums (P * ASeq)) . (((len FSeq) + 1) + k) = (Partial_Sums (P * ASeq)) . (len FSeq) ; :: thesis: S

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

now :: thesis: for n being Nat holds (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n

then A15:
for n being Nat holds (Partial_Sums (P * (Partial_Diff_Union ASeq))) . n <= (Partial_Sums (P * ASeq)) . n
by SERIES_1:14;let n be 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;(Partial_Diff_Union ASeq) . n c= ASeq . n by Th17;

hence (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n by Th5; :: thesis: verum

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: S

A18: for k being Nat holds S

A19: for m being Nat st (len FSeq) + 1 <= m holds

(Partial_Sums (P * ASeq)) . m = (Partial_Sums (P * ASeq)) . (len FSeq)

proof

then A20:
lim (Partial_Sums (P * ASeq)) = (Partial_Sums (P * ASeq)) . (len FSeq)
by Th3;
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;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

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

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

proof

end;

Partial_Sums (P * ASeq) is convergent
by A19, Th3;now :: thesis: Sum (P * FSeq) = Sum (P * ASeq)end;

hence
Sum (P * FSeq) = Sum (P * ASeq)
; :: thesis: verumper cases
( len FSeq = 0 or len FSeq <> 0 )
;

end;

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;hence Sum (P * FSeq) = Sum (P * ASeq) by Th62; :: thesis: verum

suppose A23:
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 S_{2}[ object , object ] 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)) ) )

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 S_{3}[ Nat] means seq2 . $1 = (Partial_Sums (P * ASeq)) . $1;

A31: for k being Nat st S_{3}[k] holds

S_{3}[k + 1]

.= (Partial_Sums (P * ASeq)) . 0 by SERIES_1:def 1 ;

then A38: S_{3}[ 0 ]
;

A39: for k being Nat holds S_{3}[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;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 S

( 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

then consider seq2 being Real_Sequence such that
A28:
for x being object st x in NAT holds

ex y being object st S_{2}[x,y]

A29: ( dom f = NAT & ( for x being object st x in NAT holds

S_{2}[x,f . x] ) )
from CLASSES1:sch 1(A28);

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;ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in NAT implies ex y being object st S_{2}[x,y] )

assume x in NAT ; :: thesis: ex y being object st S_{2}[x,y]

then reconsider n = x as Element of NAT ;

_{2}[x,y]
; :: thesis: verum

end;assume x in NAT ; :: thesis: ex y being object st S

then reconsider n = x as Element of NAT ;

now :: thesis: ( ( n = 0 & S_{2}[x, 0 ] ) or ( n <> 0 & n <= len (P * FSeq) & S_{2}[x,seq1 . n] ) or ( n <> 0 & not n <= len (P * FSeq) & S_{2}[x,(Partial_Sums (P * ASeq)) . (len (P * FSeq))] ) )

hence
ex y being object st Send;

A29: ( dom f = NAT & ( for x being object st x in NAT holds

S

now :: thesis: for x being object st x in NAT holds

f . x is real

then reconsider f = f as Real_Sequence by A29, SEQ_1:1;f . x is real

let x be object ; :: 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;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

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

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 S

A31: for k being Nat st S

S

proof

seq2 . 0 =
(P * ASeq) . 0
by A4, A30
let k be Nat; :: thesis: ( S_{3}[k] implies S_{3}[k + 1] )

assume A32: S_{3}[k]
; :: thesis: S_{3}[k + 1]

_{3}[k + 1]
; :: thesis: verum

end;assume A32: S

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) ) )end;

hence
Sper cases
( k = 0 or ( k <> 0 & k <= (len (P * FSeq)) - 1 ) or ( k <> 0 & not k <= (len (P * FSeq)) - 1 ) )
;

end;

case A33:
( 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, A33, A35, NAT_1:14 ;

:: thesis: verum

end;then A35: k < len FSeq by Th61;

k + 1 <= ((len (P * FSeq)) - 1) + 1 by A33, XREAL_1:7;

hence seq2 . (k + 1) = seq1 . (k + 1) by A30

.= (seq1 . k) + ((P * FSeq) . (k + 1)) by A26, A33, A34

.= ((Partial_Sums (P * ASeq)) . k) + ((P * FSeq) . (k + 1)) by A30, A32, A33, A34

.= (Partial_Sums (P * ASeq)) . (k + 1) by A8, A33, A35, NAT_1:14 ;

:: thesis: verum

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;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

.= (Partial_Sums (P * ASeq)) . 0 by SERIES_1:def 1 ;

then A38: S

A39: for k being Nat holds S

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

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