let X be non empty set ; :: thesis: 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) ) )
let f, g, h be PartFunc of X,ExtREAL; :: thesis: ( f is nonnegative & g is nonnegative & h is nonnegative implies ( 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) ) ) )
assume that
A1: f is nonnegative and
A2: g is nonnegative and
A3: h is nonnegative ; :: thesis: ( 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) ) )
A4: f + g is nonnegative by A1, A2, Th22;
then A5: dom ((f + g) + h) = (dom (f + g)) /\ (dom h) by A3, Th22;
hence dom ((f + g) + h) = ((dom f) /\ (dom g)) /\ (dom h) by A1, A2, Th22; :: thesis: ( (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) ) )
thus (f + g) + h is nonnegative by A3, A4, Th22; :: thesis: for x being set st x in ((dom f) /\ (dom g)) /\ (dom h) holds
((f + g) + h) . x = ((f . x) + (g . x)) + (h . x)
hereby :: thesis: verum
let x be set ; :: thesis: ( x in ((dom f) /\ (dom g)) /\ (dom h) implies ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) )
assume x in ((dom f) /\ (dom g)) /\ (dom h) ; :: thesis: ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x)
then A6: x in (dom (f + g)) /\ (dom h) by A1, A2, Th22;
then A7: x in dom (f + g) by XBOOLE_0:def 4;
thus ((f + g) + h) . x = ((f + g) . x) + (h . x) by A5, A6, MESFUNC1:def 3
.= ((f . x) + (g . x)) + (h . x) by A7, MESFUNC1:def 3 ; :: thesis: verum
end;