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)

( 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;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