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

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

hence P * ASeq is non-increasing by SEQM_3:8; :: thesis: verum