let X be non empty set ; :: thesis: for f, g, h being PartFunc of X,REAL st f is nonnegative & g is nonnegative & h is nonnegative holds
(f + g) + h is nonnegative
let f, g, h be PartFunc of X,REAL; :: thesis: ( f is nonnegative & g is nonnegative & h is nonnegative implies (f + g) + h is nonnegative )
assume that
A1: ( f is nonnegative & g is nonnegative ) and
A2: h is nonnegative ; :: thesis: (f + g) + h is nonnegative
f + g is nonnegative by A1, Th56;
hence (f + g) + h is nonnegative by A2, Th56; :: thesis: verum