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 - 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 - g) holds
g . x <= f . x ) implies f - g is nonnegative )
A1: dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12;
assume for x being set st x in dom (f - g) holds
g . x <= f . x ; :: thesis: f - g is nonnegative
hence f - g is nonnegative by A1, Th58; :: thesis: verum