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