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 P * FSeq is FinSequence of REAL
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL
let P be Probability of Sigma; :: thesis: for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL
let FSeq be FinSequence of Sigma; :: thesis: P * FSeq is FinSequence of REAL
dom (P * FSeq) = dom FSeq by Th59;
then ex n being Nat st dom (P * FSeq) = Seg n by FINSEQ_1:def 2;
then reconsider RSeq = P * FSeq as FinSequence by FINSEQ_1:def 2;
rng (P * FSeq) c= REAL ;
then rng RSeq c= REAL ;
hence P * FSeq is FinSequence of REAL by FINSEQ_1:def 4; :: thesis: verum