let a be Complex; :: thesis: for A being non empty set
for f, g being Element of PFuncs (A,COMPLEX) holds (addcpfunc A) . (((multcomplexcpfunc A) . (a,f)),((multcomplexcpfunc A) . (a,g))) = (multcomplexcpfunc A) . (a,((addcpfunc A) . (f,g)))
let A be non empty set ; :: thesis: for f, g being Element of PFuncs (A,COMPLEX) holds (addcpfunc A) . (((multcomplexcpfunc A) . (a,f)),((multcomplexcpfunc A) . (a,g))) = (multcomplexcpfunc A) . (a,((addcpfunc A) . (f,g)))
let f, g be Element of PFuncs (A,COMPLEX); :: thesis: (addcpfunc A) . (((multcomplexcpfunc A) . (a,f)),((multcomplexcpfunc A) . (a,g))) = (multcomplexcpfunc A) . (a,((addcpfunc A) . (f,g)))
reconsider a = a as Element of COMPLEX by XCMPLX_0:def 2;
reconsider h = (multcomplexcpfunc A) . (a,f) as Element of PFuncs (A,COMPLEX) ;
reconsider i = (multcomplexcpfunc A) . (a,g) as Element of PFuncs (A,COMPLEX) ;
set j = (addcpfunc A) . (f,g);
reconsider k = (multcomplexcpfunc A) . (a,((addcpfunc A) . (f,g))) as Element of PFuncs (A,COMPLEX) ;
set l = (addcpfunc A) . (h,i);
A1: ( dom h = dom f & dom i = dom g ) by Th7;
A2: dom ((addcpfunc A) . (h,i)) = (dom h) /\ (dom i) by Th4;
A3: dom ((addcpfunc A) . (f,g)) = (dom f) /\ (dom g) by Th4;

A4: now :: thesis: for x being Element of A st x in dom ((addcpfunc A) . (h,i)) holds
((addcpfunc A) . (h,i)) . x = k . x

let x be Element of A; :: thesis: ( x in dom ((addcpfunc A) . (h,i)) implies ((addcpfunc A) . (h,i)) . x = k . x )
A5: h . x = (a (#) f) . x by Def4;
assume A6: x in dom ((addcpfunc A) . (h,i)) ; :: thesis: ((addcpfunc A) . (h,i)) . x = k . x
then A7: x in dom (f + g) by A1, A2, VALUED_1:def 1;
A8: i . x = (a (#) g) . x by Def4;
x in dom i by A2, A6, XBOOLE_0:def 4;
then x in dom g by Th7;
then x in dom (a (#) g) by VALUED_1:def 5;
then A9: i . x = a * (g . x) by A8, VALUED_1:def 5;
x in dom h by A2, A6, XBOOLE_0:def 4;
then x in dom f by Th7;
then x in dom (a (#) f) by VALUED_1:def 5;
then A10: h . x = a * (f . x) by A5, VALUED_1:def 5;
thus ((addcpfunc A) . (h,i)) . x = (h . x) + (i . x) by A6, Th4
.= a * ((f . x) + (g . x)) by A10, A9
.= a * ((f + g) . x) by A7, VALUED_1:def 1
.= a * (((addcpfunc A) . (f,g)) . x) by Def5
.= k . x by A1, A3, A2, A6, Th7 ; :: thesis: verum

end;

dom k = dom ((addcpfunc A) . (f,g)) by Th7;
hence (addcpfunc A) . (((multcomplexcpfunc A) . (a,f)),((multcomplexcpfunc A) . (a,g))) = (multcomplexcpfunc A) . (a,((addcpfunc A) . (f,g))) by A1, A3, A2, A4, PARTFUN1:5; :: thesis: verum