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 A1: ( f is without+infty & g is without+infty ) ; :: thesis: f + g is without+infty
then P2: dom (f + g) = (dom f) /\ (dom g) by M5th22;
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 B1: x in dom (f + g) ; :: thesis: (f + g) . x < +infty
then ( x in dom f & x in dom g ) by P2, XBOOLE_0:def 4;
then B2: ( f . x < +infty & g . x < +infty ) by A1, MESFUNC5:17;
(f + g) . x = (f . x) + (g . x) by B1, MESFUNC1:def 3;
hence (f + g) . x < +infty by B2, XXREAL_0:4, XXREAL_3:16; :: thesis: verum

end;

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