let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S 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 S st SSets is non-descending holds
M * SSets is non-decreasing

let M be sigma_Measure of S; :: thesis: for SSets being SetSequence of S st SSets is non-descending holds
M * SSets is non-decreasing

let SSets be SetSequence of S; :: thesis: ( SSets is non-descending implies M * SSets is non-decreasing )
A1: dom (M * SSets) = NAT by FUNCT_2:def 1;
assume A2: SSets is non-descending ; :: thesis: M * SSets is non-decreasing
now :: thesis: for n, m being Nat st n <= m holds
(M * SSets) . n <= (M * SSets) . m
let n, m be Nat; :: thesis: ( n <= m implies (M * SSets) . n <= (M * SSets) . m )
A3: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
A4: (M * SSets) . m = M . (SSets . m) by ;
assume n <= m ; :: thesis: (M * SSets) . n <= (M * SSets) . m
then A5: SSets . n c= SSets . m by ;
( rng SSets c= S & (M * SSets) . n = M . (SSets . n) ) by ;
hence (M * SSets) . n <= (M * SSets) . m by ; :: thesis: verum
end;
then for n, m being Nat st m <= n holds
(M * SSets) . m <= (M * SSets) . n ;
hence M * SSets is non-decreasing by RINFSUP2:7; :: thesis: verum