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

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