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 V77() 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 V77() 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 V77() 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 V77() holds

(P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n

let P be Probability of Sigma; :: thesis: ( ASeq is V77() implies (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n )

A1: dom (P * ASeq) = NAT by SEQ_1:1;

defpred S_{1}[ 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 V77() ; :: thesis: (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n

A4: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by Th40;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A8, A4);

hence (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n ; :: thesis: verum

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() 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 V77() 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 V77() 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 V77() holds

(P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n

let P be Probability of Sigma; :: thesis: ( ASeq is V77() implies (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n )

A1: dom (P * ASeq) = NAT by SEQ_1:1;

defpred S

A2: dom (P * (Partial_Union ASeq)) = NAT by SEQ_1:1;

assume A3: ASeq is V77() ; :: thesis: (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n

A4: for k being Nat st S

S

proof

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

assume A5: (P * (Partial_Union ASeq)) . k = (Partial_Sums (P * ASeq)) . k ; :: thesis: S_{1}[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 S_{1}[k + 1]
by A5, A7; :: thesis: verum

end;assume A5: (P * (Partial_Union ASeq)) . k = (Partial_Sums (P * ASeq)) . k ; :: thesis: S

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 S

for k being Nat holds S

hence (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n ; :: thesis: verum