let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st f is nonnegative & g is nonnegative holds
( dom (f + g) = (dom f) /\ (dom g) & f + g is nonnegative )
let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is nonnegative & g is nonnegative implies ( dom (f + g) = (dom f) /\ (dom g) & f + g is nonnegative ) )
assume that
A1: f is nonnegative and
A2: g is nonnegative ; :: thesis: ( dom (f + g) = (dom f) /\ (dom g) & f + g is nonnegative )
thus A3: dom (f + g) = (dom f) /\ (dom g) by A1, A2, Th16; :: thesis: f + g is nonnegative

now :: thesis: for x being object st x in (dom f) /\ (dom g) holds
0 <= (f + g) . x

let x be object ; :: thesis: ( x in (dom f) /\ (dom g) implies 0 <= (f + g) . x )
assume A4: x in (dom f) /\ (dom g) ; :: thesis: 0 <= (f + g) . x
A5: 0 <= g . x by A2, SUPINF_2:51;
0 <= f . x by A1, SUPINF_2:51;
then 0 <= (f . x) + (g . x) by A5;
hence 0 <= (f + g) . x by A3, A4, MESFUNC1:def 3; :: thesis: verum

end;

hence f + g is nonnegative by A3, SUPINF_2:52; :: thesis: verum