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 )
assume A1: ASeq . n c= BSeq . n ; :: thesis: (P * ASeq) . n <= (P * BSeq) . n
A2: n in NAT by ORDINAL1:def 13;
X: ( ASeq . n in rng ASeq & BSeq . n in rng BSeq ) by NAT_1:52;
( rng ASeq c= Sigma & rng BSeq c= Sigma ) by PROB_1:def 9;
then ( ASeq . n in Sigma & BSeq . n in Sigma ) by X;
then ( ASeq . n is Event of Sigma & BSeq . n is Event of Sigma ) ;
then P . (ASeq . n) <= P . (BSeq . n) by A1, PROB_1:70;
then (P * ASeq) . n <= P . (BSeq . n) by A2, FUNCT_2:21;
hence (P * ASeq) . n <= (P * BSeq) . n by A2, FUNCT_2:21; :: thesis: verum