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

A3: now :: thesis: for x being Element of A st x in dom ((multcpfunc A) . (i,g)) holds
((multcpfunc A) . (i,g)) . x = l . x

let x be Element of A; :: thesis: ( x in dom ((multcpfunc A) . (i,g)) implies ((multcpfunc A) . (i,g)) . x = l . x )
A4: ((multcpfunc A) . (f,g)) . x = (f (#) g) . x by Def3;
assume A5: x in dom ((multcpfunc A) . (i,g)) ; :: thesis: ((multcpfunc A) . (i,g)) . x = l . x
then x in dom (f (#) g) by A1, VALUED_1:def 4;
then A6: ((multcpfunc A) . (f,g)) . x = (f . x) * (g . x) by A4, VALUED_1:def 4;
A7: ( i . x = (a (#) f) . x & dom (a (#) f) = dom f ) by Def4, VALUED_1:def 5;
x in dom f by A1, A5, XBOOLE_0:def 4;
then A8: i . x = a * (f . x) by A7, VALUED_1:def 5;
A9: l . x = (a (#) ((multcpfunc A) . (f,g))) . x by Def4;
x in dom (a (#) ((multcpfunc A) . (f,g))) by A1, A2, A5, VALUED_1:def 5;
then A10: l . x = a * ((f . x) * (g . x)) by A6, A9, VALUED_1:def 5;
((multcpfunc A) . (i,g)) . x = (i . x) * (g . x) by A5, Th5;
hence ((multcpfunc A) . (i,g)) . x = l . x by A8, A10; :: thesis: verum

end;

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