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 A1: ( f is nonnegative & g is nonnegative & h is nonnegative ) ; :: thesis: (f + g) + h is nonnegative
then f + g is nonnegative by Th56;
hence (f + g) + h is nonnegative by A1, Th56; :: thesis: verum