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 non-descending 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 non-descending holds
P * ASeq is non-decreasing
let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma st ASeq is non-descending holds
P * ASeq is non-decreasing
let P be Probability of Sigma; :: thesis: ( ASeq is non-descending implies P * ASeq is non-decreasing )
A1: dom (P * ASeq) = NAT by SEQ_1:1;
assume A2: ASeq is non-descending ; :: thesis: P * ASeq is non-decreasing

now :: thesis: for n, m being Nat st n <= m holds
(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;

hence P * ASeq is non-decreasing by SEQM_3:6; :: thesis: verum