let X be non empty set ; :: thesis: for f, g being PartFunc of X,REAL st ( for x being set st x in dom f holds
f . x <= g . x ) holds
g - f is nonnegative
let f, g be PartFunc of X,REAL; :: thesis: ( ( for x being set st x in dom f holds
f . x <= g . x ) implies g - f is nonnegative )
assume A1: for x being set st x in dom f holds
f . x <= g . x ; :: thesis: g - f is nonnegative

now :: thesis: for x being object st x in dom (g - f) holds
0 <= (g - f) . x

let x be object ; :: thesis: ( x in dom (g - f) implies 0 <= (g - f) . x )
assume A2: x in dom (g - f) ; :: thesis: 0 <= (g - f) . x
then x in (dom g) /\ (dom f) by VALUED_1:12;
then x in dom f by XBOOLE_0:def 4;
then 0 <= (g . x) - (f . x) by A1, XREAL_1:48;
hence 0 <= (g - f) . x by A2, VALUED_1:13; :: thesis: verum

end;

hence g - f is nonnegative by MESFUNC6:52; :: thesis: verum