let X be set ; :: thesis: for F being Field_Subset of X

for M being Measure of F

for FSets being Set_Sequence of F st FSets is non-descending holds

M * FSets is non-decreasing

let F be Field_Subset of X; :: thesis: for M being Measure of F

for FSets being Set_Sequence of F st FSets is non-descending holds

M * FSets is non-decreasing

let M be Measure of F; :: thesis: for FSets being Set_Sequence of F st FSets is non-descending holds

M * FSets is non-decreasing

let FSets be Set_Sequence of F; :: thesis: ( FSets is non-descending implies M * FSets is non-decreasing )

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

assume A2: FSets is non-descending ; :: thesis: M * FSets is non-decreasing

(M * FSets) . m <= (M * FSets) . n ;

hence M * FSets is non-decreasing by RINFSUP2:7; :: thesis: verum

for M being Measure of F

for FSets being Set_Sequence of F st FSets is non-descending holds

M * FSets is non-decreasing

let F be Field_Subset of X; :: thesis: for M being Measure of F

for FSets being Set_Sequence of F st FSets is non-descending holds

M * FSets is non-decreasing

let M be Measure of F; :: thesis: for FSets being Set_Sequence of F st FSets is non-descending holds

M * FSets is non-decreasing

let FSets be Set_Sequence of F; :: thesis: ( FSets is non-descending implies M * FSets is non-decreasing )

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

assume A2: FSets is non-descending ; :: thesis: M * FSets is non-decreasing

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

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

then
for n, m being Nat st m <= n holds (M * FSets) . n <= (M * FSets) . m

let n, m be Nat; :: thesis: ( n <= m implies (M * FSets) . n <= (M * FSets) . m )

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

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

then A4: FSets . n c= FSets . m by A2, PROB_1:def 5;

( (M * FSets) . n = M . (FSets . n) & (M * FSets) . m = M . (FSets . m) ) by A1, FUNCT_1:12, A3;

hence (M * FSets) . n <= (M * FSets) . m by A4, MEASURE1:8; :: thesis: verum

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

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

then A4: FSets . n c= FSets . m by A2, PROB_1:def 5;

( (M * FSets) . n = M . (FSets . n) & (M * FSets) . m = M . (FSets . m) ) by A1, FUNCT_1:12, A3;

hence (M * FSets) . n <= (M * FSets) . m by A4, MEASURE1:8; :: thesis: verum

(M * FSets) . m <= (M * FSets) . n ;

hence M * FSets is non-decreasing by RINFSUP2:7; :: thesis: verum