let X be set ; :: thesis: for Y being complex-functions-membered set
for c1, c2 being Complex
for f being PartFunc of X,Y holds (f [+] c1) [+] c2 = f [+] (c1 + c2)

let Y be complex-functions-membered set ; :: thesis: for c1, c2 being Complex
for f being PartFunc of X,Y holds (f [+] c1) [+] c2 = f [+] (c1 + c2)

let c1, c2 be Complex; :: thesis: for f being PartFunc of X,Y holds (f [+] c1) [+] c2 = f [+] (c1 + c2)
let f be PartFunc of X,Y; :: thesis: (f [+] c1) [+] c2 = f [+] (c1 + c2)
set f1 = f [+] c1;
A1: dom ((f [+] c1) [+] c2) = dom (f [+] c1) by Def37;
dom (f [+] c1) = dom f by Def37;
hence A2: dom ((f [+] c1) [+] c2) = dom (f [+] (c1 + c2)) by ; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom ((f [+] c1) [+] c2) or ((f [+] c1) [+] c2) . b1 = (f [+] (c1 + c2)) . b1 )

let x be object ; :: thesis: ( not x in dom ((f [+] c1) [+] c2) or ((f [+] c1) [+] c2) . x = (f [+] (c1 + c2)) . x )
assume A3: x in dom ((f [+] c1) [+] c2) ; :: thesis: ((f [+] c1) [+] c2) . x = (f [+] (c1 + c2)) . x
hence ((f [+] c1) [+] c2) . x = ((f [+] c1) . x) + c2 by Def37
.= ((f . x) + c1) + c2 by
.= (f . x) + (c1 + c2) by Th12
.= (f [+] (c1 + c2)) . x by ;
:: thesis: verum