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 )
assume A1: FSets is non-descending ; :: thesis: M * FSets is non-decreasing
A2: dom (M * FSets) = NAT by FUNCT_2:def 1;

now

let n, m be Element of NAT ; :: thesis: ( n <= m implies (M * FSets) . n <= (M * FSets) . m )
assume n <= m ; :: thesis: (M * FSets) . n <= (M * FSets) . m
then A5: FSets . n c= FSets . m by A1, PROB_1:def 7;
( (M * FSets) . n = M . (FSets . n) & (M * FSets) . m = M . (FSets . m) ) by A2, FUNCT_1:22;
hence (M * FSets) . n <= (M * FSets) . m by A5, MEASURE1:25; :: thesis: verum

end;

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