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