let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st f is V124() & g is V123() holds
f - g is V124()
let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is V124() & g is V123() implies f - g is V124() )
assume that
A1: f is V124() and
A2: g is V123() ; :: thesis: f - g is V124()
for x being set st x in dom (f - g) holds
(f - g) . x < +infty

proof

let x be set ; :: thesis: ( x in dom (f - g) implies (f - g) . x < +infty )
assume A3: x in dom (f - g) ; :: thesis: (f - g) . x < +infty
A4: f . x < +infty by A1;
A5: -infty < g . x by A2;
(f - g) . x = (f . x) - (g . x) by A3, MESFUNC1:def 4;
hence (f - g) . x < +infty by A4, A5, XXREAL_0:4, XXREAL_3:18; :: thesis: verum

end;

hence f - g is V124() by MESFUNC5:11; :: thesis: verum