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-ascending holds
M * FSets is non-increasing

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-ascending holds
M * FSets is non-increasing

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

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