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 A1: ( f is nonnegative & g is nonnegative ) ; :: thesis: ( dom (f + g) = (dom f) /\ (dom g) & f + g is nonnegative )
then ( ( for x being set st x in dom f holds
-infty < f . x ) & ( for x being set st x in dom g holds
-infty < g . x ) ) by SUPINF_2:70;
then ( f is without-infty & g is without-infty ) by Th16;
hence A2: dom (f + g) = (dom f) /\ (dom g) by Th22; :: thesis: f + g is nonnegative

now

let x be set ; :: thesis: ( x in (dom f) /\ (dom g) implies 0 <= (f + g) . x )
assume A3: x in (dom f) /\ (dom g) ; :: thesis: 0 <= (f + g) . x
( 0 <= f . x & 0 <= g . x ) by A1, SUPINF_2:70;
then 0 <= (f . x) + (g . x) by EXTREAL2:7;
hence 0 <= (f + g) . x by A2, A3, MESFUNC1:def 3; :: thesis: verum

end;

hence f + g is nonnegative by A2, SUPINF_2:71; :: thesis: verum