let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st f is V125() & g is V125() holds
f + g is V125()
let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is V125() & g is V125() implies f + g is V125() )
assume that
A1: f is V125() and
A2: g is V125() ; :: thesis: f + g is V125()
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 V125() by MESFUNC5:11; :: thesis: verum