let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st f is without+infty & g is without+infty holds
f + g is without+infty
let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is without+infty & g is without+infty implies f + g is without+infty )
assume that
A1: f is without+infty and
A2: g is without+infty ; :: thesis: f + g is without+infty
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: g . x < +infty by A2;
(f + g) . x = (f . x) + (g . x) by A3, MESFUNC1:def 3;
hence (f + g) . x < +infty by A4, A5, XXREAL_0:4, XXREAL_3:16; :: thesis: verum

end;

hence f + g is without+infty by MESFUNC5:11; :: thesis: verum