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

for Sigma being SigmaField of Omega

for ASeq, BSeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq . n c= BSeq . n holds

(P * ASeq) . n <= (P * BSeq) . n

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

for ASeq, BSeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq . n c= BSeq . n holds

(P * ASeq) . n <= (P * BSeq) . n

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

for P being Probability of Sigma st ASeq . n c= BSeq . n holds

(P * ASeq) . n <= (P * BSeq) . n

let ASeq, BSeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma st ASeq . n c= BSeq . n holds

(P * ASeq) . n <= (P * BSeq) . n

let P be Probability of Sigma; :: thesis: ( ASeq . n c= BSeq . n implies (P * ASeq) . n <= (P * BSeq) . n )

A1: n in NAT by ORDINAL1:def 12;

assume ASeq . n c= BSeq . n ; :: thesis: (P * ASeq) . n <= (P * BSeq) . n

then P . (ASeq . n) <= P . (BSeq . n) by PROB_1:34;

then (P * ASeq) . n <= P . (BSeq . n) by A1, FUNCT_2:15;

hence (P * ASeq) . n <= (P * BSeq) . n by A1, FUNCT_2:15; :: thesis: verum

for Sigma being SigmaField of Omega

for ASeq, BSeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq . n c= BSeq . n holds

(P * ASeq) . n <= (P * BSeq) . n

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

for ASeq, BSeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq . n c= BSeq . n holds

(P * ASeq) . n <= (P * BSeq) . n

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

for P being Probability of Sigma st ASeq . n c= BSeq . n holds

(P * ASeq) . n <= (P * BSeq) . n

let ASeq, BSeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma st ASeq . n c= BSeq . n holds

(P * ASeq) . n <= (P * BSeq) . n

let P be Probability of Sigma; :: thesis: ( ASeq . n c= BSeq . n implies (P * ASeq) . n <= (P * BSeq) . n )

A1: n in NAT by ORDINAL1:def 12;

assume ASeq . n c= BSeq . n ; :: thesis: (P * ASeq) . n <= (P * BSeq) . n

then P . (ASeq . n) <= P . (BSeq . n) by PROB_1:34;

then (P * ASeq) . n <= P . (BSeq . n) by A1, FUNCT_2:15;

hence (P * ASeq) . n <= (P * BSeq) . n by A1, FUNCT_2:15; :: thesis: verum