let X be set ; :: thesis: for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g, h being complex-valued Function holds (f <+> g) <+> h = f <+> (g + h)

let Y be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y
for g, h being complex-valued Function holds (f <+> g) <+> h = f <+> (g + h)

let f be PartFunc of X,Y; :: thesis: for g, h being complex-valued Function holds (f <+> g) <+> h = f <+> (g + h)
let g, h be complex-valued Function; :: thesis: (f <+> g) <+> h = f <+> (g + h)
set f1 = f <+> g;
A1: dom (g + h) = (dom g) /\ (dom h) by VALUED_1:def 1;
A2: dom ((f <+> g) <+> h) = (dom (f <+> g)) /\ (dom h) by Def41;
( dom (f <+> g) = (dom f) /\ (dom g) & dom (f <+> (g + h)) = (dom f) /\ (dom (g + h)) ) by Def41;
hence A3: dom ((f <+> g) <+> h) = dom (f <+> (g + h)) by ; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom ((f <+> g) <+> h) or ((f <+> g) <+> h) . b1 = (f <+> (g + h)) . b1 )

let x be object ; :: thesis: ( not x in dom ((f <+> g) <+> h) or ((f <+> g) <+> h) . x = (f <+> (g + h)) . x )
assume A4: x in dom ((f <+> g) <+> h) ; :: thesis: ((f <+> g) <+> h) . x = (f <+> (g + h)) . x
then A5: x in dom (f <+> g) by ;
A6: x in dom (g + h) by ;
thus ((f <+> g) <+> h) . x = ((f <+> g) . x) + (h . x) by
.= ((f . x) + (g . x)) + (h . x) by
.= (f . x) + ((g . x) + (h . x)) by Th12
.= (f . x) + ((g + h) . x) by
.= (f <+> (g + h)) . x by ; :: thesis: verum