let X be non empty set ; :: thesis: for f, g, h being PartFunc of X,REAL
for x being object st x in dom ((f + g) + h) holds
((f + g) + h) . x = ((f . x) + (g . x)) + (h . x)
let f, g, h be PartFunc of X,REAL; :: thesis: for x being object st x in dom ((f + g) + h) holds
((f + g) + h) . x = ((f . x) + (g . x)) + (h . x)
let x be object ; :: thesis: ( x in dom ((f + g) + h) implies ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) )
assume A1: x in dom ((f + g) + h) ; :: thesis: ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x)
dom ((f + g) + h) = (dom (f + g)) /\ (dom h) by VALUED_1:def 1;
then x in dom (f + g) by A1, XBOOLE_0:def 4;
then ((f . x) + (g . x)) + (h . x) = ((f + g) . x) + (h . x) by VALUED_1:def 1;
hence ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) by A1, VALUED_1:def 1; :: thesis: verum