let n be Nat; :: thesis: for Omega being non empty set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * ASeq) . n >= 0

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

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * ASeq) . n >= 0

let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * ASeq) . n >= 0

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds (P * ASeq) . n >= 0

let P be Probability of Sigma; :: thesis: (P * ASeq) . n >= 0

A1: n in NAT by ORDINAL1:def 12;

dom (P * ASeq) = NAT by SEQ_1:1;

then (P * ASeq) . n = P . (ASeq . n) by A1, FUNCT_1:12;

hence (P * ASeq) . n >= 0 by PROB_1:def 8; :: thesis: verum

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * ASeq) . n >= 0

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

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * ASeq) . n >= 0

let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds (P * ASeq) . n >= 0

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds (P * ASeq) . n >= 0

let P be Probability of Sigma; :: thesis: (P * ASeq) . n >= 0

A1: n in NAT by ORDINAL1:def 12;

dom (P * ASeq) = NAT by SEQ_1:1;

then (P * ASeq) . n = P . (ASeq . n) by A1, FUNCT_1:12;

hence (P * ASeq) . n >= 0 by PROB_1:def 8; :: thesis: verum