let X be non empty set ; :: thesis: for f, g being PartFunc of X,REAL st f is nonnegative & g is nonnegative holds
f + g is nonnegative
let f, g be PartFunc of X,REAL ; :: thesis: ( f is nonnegative & g is nonnegative implies f + g is nonnegative )
assume A1: ( f is nonnegative & g is nonnegative ) ; :: thesis: f + g is nonnegative
for x being set st x in dom (f + g) holds
0 <= (f + g) . x

proof

let x be set ; :: thesis: ( x in dom (f + g) implies 0 <= (f + g) . x )
assume A2: x in dom (f + g) ; :: thesis: 0 <= (f + g) . x
A3: ( 0 <= f . x & 0 <= g . x ) by A1, Th51;
then g . x <= (f . x) + (g . x) by XREAL_1:33;
hence 0 <= (f + g) . x by A2, A3, VALUED_1:def 1; :: thesis: verum

end;

hence f + g is nonnegative by Th52; :: thesis: verum