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

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

hence
g - f is nonnegative
by MESFUNC6:52; :: thesis: verum0 <= (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;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