let a, b be Complex; :: thesis:
let A be non empty set ; :: thesis:
let f be Element of PFuncs (A,COMPLEX); :: thesis:
reconsider a = a, b = b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider c = a + b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider g = (multcomplexcpfunc A) . (a,f) as Element of PFuncs (A,COMPLEX) ;
reconsider h = (multcomplexcpfunc A) . (b,f) as Element of PFuncs (A,COMPLEX) ;
reconsider k = (multcomplexcpfunc A) . (c,f) as Element of PFuncs (A,COMPLEX) ;
set j = (addcpfunc A) . (g,h);
dom g = dom f by Th7;
then (dom h) /\ (dom g) = (dom f) /\ (dom f) by Th7;
then A1: dom ((addcpfunc A) . (g,h)) = dom f by Th4;

let x be Element of A; :: thesis:
assume A3: x in dom ((addcpfunc A) . (g,h)) ; :: thesis:
then x in dom (b (#) f) by A1, VALUED_1:def 5;
then (b (#) f) . x = b * (f . x) by VALUED_1:def 5;
then A4: h . x = b * (f . x) by Def4;
x in dom (a (#) f) by A1, A3, VALUED_1:def 5;
then (a (#) f) . x = a * (f . x) by VALUED_1:def 5;
then g . x = a * (f . x) by Def4;
then (g . x) + (h . x) = (a + b) * (f . x) by A4;
hence ((addcpfunc A) . (g,h)) . x = (a + b) * (f . x) by A3, Th4
.= k . x by A1, A3, Th7 ;
:: thesis:

end;