let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of st SSets is non-descending holds
M * SSets is non-decreasing
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for SSets being SetSequence of st SSets is non-descending holds
M * SSets is non-decreasing
let M be sigma_Measure of S; :: thesis: for SSets being SetSequence of st SSets is non-descending holds
M * SSets is non-decreasing
let SSets be SetSequence of ; :: thesis: ( SSets is non-descending implies M * SSets is non-decreasing )
assume A1: SSets is non-descending ; :: thesis: M * SSets is non-decreasing
A2: dom (M * SSets) = NAT by FUNCT_2:def 1;

now

let n, m be Element of NAT ; :: thesis: ( n <= m implies (M * SSets) . n <= (M * SSets) . m )
assume n <= m ; :: thesis: (M * SSets) . n <= (M * SSets) . m
then A5: SSets . n c= SSets . m by A1, PROB_1:def 7;
A3: ( SSets . n in rng SSets & SSets . m in rng SSets ) by FUNCT_2:6;
A4: rng SSets c= S by RELAT_1:def 19;
( (M * SSets) . n = M . (SSets . n) & (M * SSets) . m = M . (SSets . m) ) by A2, FUNCT_1:22;
hence (M * SSets) . n <= (M * SSets) . m by A3, A4, A5, MEASURE1:62; :: thesis: verum

end;

then for n, m being Element of NAT st m <= n holds
(M * SSets) . m <= (M * SSets) . n ;
hence M * SSets is non-decreasing by RINFSUP2:7; :: thesis: verum