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 V75() holds

P * ASeq is non-decreasing

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

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

P * ASeq is non-decreasing

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

P * ASeq is non-decreasing

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

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

assume A2: ASeq is V75() ; :: thesis: P * ASeq is non-decreasing

for ASeq being SetSequence of Sigma

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

P * ASeq is non-decreasing

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

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

P * ASeq is non-decreasing

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

P * ASeq is non-decreasing

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

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

assume A2: ASeq is V75() ; :: thesis: P * ASeq is non-decreasing

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

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

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

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

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

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

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) . n <= (P * ASeq) . m by A3, PROB_1:34; :: thesis: verum

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

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

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) . n <= (P * ASeq) . m by A3, PROB_1:34; :: thesis: verum