for X being non empty set
for f, g being PartFunc of X,ExtREAL st ( for x being set st x in (dom f) /\ (dom g) holds
( g . x <= f . x & -infty < g . x & f . x < +infty ) ) holds
f - g is nonnegative