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 )
assume A1: ASeq is non-descending ; :: thesis: P * ASeq is non-decreasing
A2: dom (P * ASeq) = NAT by SEQ_1:3;

now

let n, m be Element of NAT ; :: thesis: ( n <= m implies (P * ASeq) . n <= (P * ASeq) . m )
assume A3: n <= m ; :: thesis: (P * ASeq) . n <= (P * ASeq) . m
A5: ASeq . n c= ASeq . m by A1, A3, PROB_1:def 7;
( (P * ASeq) . n = P . (ASeq . n) & (P * ASeq) . m = P . (ASeq . m) ) by A2, FUNCT_1:22;
hence (P * ASeq) . n <= (P * ASeq) . m by A5, PROB_1:70; :: thesis: verum

end;

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