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 st ASeq is V74() holds

P * ASeq is non-increasing

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

for P being Probability of Sigma st ASeq is V74() holds

P * ASeq is non-increasing

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma st ASeq is V74() holds

P * ASeq is non-increasing

let P be Probability of Sigma; :: thesis: ( ASeq is V74() implies P * ASeq is non-increasing )

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

assume A2: ASeq is V74() ; :: thesis: P * ASeq is non-increasing

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V74() holds

P * ASeq is non-increasing

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

for P being Probability of Sigma st ASeq is V74() holds

P * ASeq is non-increasing

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma st ASeq is V74() holds

P * ASeq is non-increasing

let P be Probability of Sigma; :: thesis: ( ASeq is V74() implies P * ASeq is non-increasing )

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

assume A2: ASeq is V74() ; :: thesis: P * ASeq is non-increasing

now :: thesis: for n, m being Nat st n <= m holds

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

hence
P * ASeq is non-increasing
by SEQM_3:8; :: thesis: verum(P * ASeq) . m <= (P * ASeq) . n

let n, m be Nat; :: thesis: ( n <= m implies (P * ASeq) . m <= (P * ASeq) . n )

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

then A3: ASeq . m c= ASeq . n by A2, PROB_1:def 4;

reconsider nn = n, mm = m as Element of NAT by ORDINAL1:def 12;

( (P * ASeq) . nn = P . (ASeq . nn) & (P * ASeq) . mm = P . (ASeq . mm) ) by A1, FUNCT_1:12;

hence (P * ASeq) . m <= (P * ASeq) . n by A3, PROB_1:34; :: thesis: verum

end;assume n <= m ; :: thesis: (P * ASeq) . m <= (P * ASeq) . n

then A3: ASeq . m c= ASeq . n by A2, PROB_1:def 4;

reconsider nn = n, mm = m as Element of NAT by ORDINAL1:def 12;

( (P * ASeq) . nn = P . (ASeq . nn) & (P * ASeq) . mm = P . (ASeq . mm) ) by A1, FUNCT_1:12;

hence (P * ASeq) . m <= (P * ASeq) . n by A3, PROB_1:34; :: thesis: verum