let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq

let P be Probability of Sigma; :: thesis: for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq

let FSeq be FinSequence of Sigma; :: thesis: len (P * FSeq) = len FSeq

dom (P * FSeq) = dom FSeq by Th59;

then Seg (len (P * FSeq)) = dom FSeq by FINSEQ_1:def 3;

hence len (P * FSeq) = len FSeq by FINSEQ_1:def 3; :: thesis: verum

for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq

let P be Probability of Sigma; :: thesis: for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq

let FSeq be FinSequence of Sigma; :: thesis: len (P * FSeq) = len FSeq

dom (P * FSeq) = dom FSeq by Th59;

then Seg (len (P * FSeq)) = dom FSeq by FINSEQ_1:def 3;

hence len (P * FSeq) = len FSeq by FINSEQ_1:def 3; :: thesis: verum