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) /\ (dom g) holds
g . x <= f . x ) holds
f - g is nonnegative
let f, g be PartFunc of X,REAL; :: thesis: ( ( for x being set st x in (dom f) /\ (dom g) holds
g . x <= f . x ) implies f - g is nonnegative )
assume A1: for x being set st x in (dom f) /\ (dom g) holds
g . x <= f . x ; :: thesis: f - g is nonnegative

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

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

end;

hence f - g is nonnegative by Th52; :: thesis: verum