theorem Th23: :: MESFUNC5:23

for X being non empty set
for f, g, h being PartFunc of X,ExtREAL st f is nonnegative & g is nonnegative & h is nonnegative holds
( dom ((f + g) + h) = ((dom f) /\ (dom g)) /\ (dom h) & (f + g) + h is nonnegative & ( for x being set st x in ((dom f) /\ (dom g)) /\ (dom h) holds
((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) ) )