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-ascending holds

M * SSets is non-increasing

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for SSets being SetSequence of S st SSets is non-ascending holds

M * SSets is non-increasing

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

M * SSets is non-increasing

let SSets be SetSequence of S; :: thesis: ( SSets is non-ascending implies M * SSets is non-increasing )

A1: dom (M * SSets) = NAT by FUNCT_2:def 1;

assume A2: SSets is non-ascending ; :: thesis: M * SSets is non-increasing

for M being sigma_Measure of S

for SSets being SetSequence of S st SSets is non-ascending holds

M * SSets is non-increasing

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for SSets being SetSequence of S st SSets is non-ascending holds

M * SSets is non-increasing

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

M * SSets is non-increasing

let SSets be SetSequence of S; :: thesis: ( SSets is non-ascending implies M * SSets is non-increasing )

A1: dom (M * SSets) = NAT by FUNCT_2:def 1;

assume A2: SSets is non-ascending ; :: thesis: M * SSets is non-increasing

now :: thesis: for n, m being Nat st m <= n holds

(M * SSets) . n <= (M * SSets) . m

hence
M * SSets is non-increasing
by RINFSUP2:7; :: thesis: verum(M * SSets) . n <= (M * SSets) . m

let n, m be Nat; :: thesis: ( m <= n 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 A1, FUNCT_1:12, A3;

assume m <= n ; :: thesis: (M * SSets) . n <= (M * SSets) . m

then A5: SSets . n c= SSets . m by A2, PROB_1:def 4;

( rng SSets c= S & (M * SSets) . n = M . (SSets . n) ) by A1, FUNCT_1:12, A3;

hence (M * SSets) . n <= (M * SSets) . m by A5, A4, MEASURE1:31; :: thesis: verum

end;A3: ( n in NAT & m in NAT ) by ORDINAL1:def 12;

A4: (M * SSets) . m = M . (SSets . m) by A1, FUNCT_1:12, A3;

assume m <= n ; :: thesis: (M * SSets) . n <= (M * SSets) . m

then A5: SSets . n c= SSets . m by A2, PROB_1:def 4;

( rng SSets c= S & (M * SSets) . n = M . (SSets . n) ) by A1, FUNCT_1:12, A3;

hence (M * SSets) . n <= (M * SSets) . m by A5, A4, MEASURE1:31; :: thesis: verum