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 holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0

let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0

let P be Probability of Sigma; :: thesis: (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0

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

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

then A2: (P * (Partial_Union ASeq)) . 0 = P . ((Partial_Union ASeq) . 0) by FUNCT_1:12

.= P . (ASeq . 0) by Def2 ;

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

.= P . (ASeq . 0) by A1, FUNCT_1:12 ;

hence (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0 by A2; :: thesis: verum

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0

let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0

let P be Probability of Sigma; :: thesis: (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0

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

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

then A2: (P * (Partial_Union ASeq)) . 0 = P . ((Partial_Union ASeq) . 0) by FUNCT_1:12

.= P . (ASeq . 0) by Def2 ;

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

.= P . (ASeq . 0) by A1, FUNCT_1:12 ;

hence (P * (Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0 by A2; :: thesis: verum