let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom f holds
f . x <= g . x ) holds
g - f is nonnegative
let f, g be PartFunc of X,ExtREAL; :: thesis: ( ( for x being Element of X st x in dom f holds
f . x <= g . x ) implies g - f is nonnegative )
assume A1: for x being Element of X st x in dom f holds
f . x <= g . x ; :: thesis: g - f is nonnegative
now :: thesis: for y being ExtReal st y in rng (g - f) holds
0 <= y
let y be ExtReal; :: thesis: ( y in rng (g - f) implies 0 <= y )
assume y in rng (g - f) ; :: thesis: 0 <= y
then consider x being object such that
A2: x in dom (g - f) and
A3: y = (g - f) . x by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
dom (g - f) = ((dom g) /\ (dom f)) \ (((g " {+infty}) /\ (f " {+infty})) \/ ((g " {-infty}) /\ (f " {-infty}))) by MESFUNC1:def 4;
then x in (dom g) /\ (dom f) by A2, XBOOLE_0:def 5;
then x in dom f by XBOOLE_0:def 4;
then 0. <= (g . x) - (f . x) by A1, XXREAL_3:40;
hence 0 <= y by A2, A3, MESFUNC1:def 4; :: thesis: verum
end;
then rng (g - f) is nonnegative by SUPINF_2:def 9;
hence g - f is nonnegative by SUPINF_2:def 12; :: thesis: verum