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