let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of
for P being Probability of Sigma st ASeq is disjoint_valued holds
P * (@Partial_Union ASeq) = Partial_Sums (P * ASeq)
let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of
for P being Probability of Sigma st ASeq is disjoint_valued holds
P * (@Partial_Union ASeq) = Partial_Sums (P * ASeq)
let ASeq be SetSequence of ; :: thesis: for P being Probability of Sigma st ASeq is disjoint_valued holds
P * (@Partial_Union ASeq) = Partial_Sums (P * ASeq)
let P be Probability of Sigma; :: thesis: ( ASeq is disjoint_valued implies P * (@Partial_Union ASeq) = Partial_Sums (P * ASeq) )
assume ASeq is disjoint_valued ; :: thesis: P * (@Partial_Union ASeq) = Partial_Sums (P * ASeq)
then for n being Element of NAT holds (P * (@Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n by Th48;
hence P * (@Partial_Union ASeq) = Partial_Sums (P * ASeq) by FUNCT_2:113; :: thesis: verum