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 disjoint_valued 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 disjoint_valued 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 disjoint_valued 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 disjoint_valued holds
(P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n
let P be Probability of Sigma; :: thesis: ( ASeq is disjoint_valued implies (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n )
A1: dom (P * ASeq) = NAT by SEQ_1:1;
defpred S₁[ 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 disjoint_valued ; :: thesis: (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

end;

A8: S₁[ 0 ] by Th40;
for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A4);
hence (P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n ; :: thesis: verum