let a, b be Complex; :: thesis: for A being non empty set
for f being Element of PFuncs (A,COMPLEX) holds (multcomplexcpfunc A) . (a,((multcomplexcpfunc A) . (b,f))) = (multcomplexcpfunc A) . ((a * b),f)
let A be non empty set ; :: thesis: for f being Element of PFuncs (A,COMPLEX) holds (multcomplexcpfunc A) . (a,((multcomplexcpfunc A) . (b,f))) = (multcomplexcpfunc A) . ((a * b),f)
let f be Element of PFuncs (A,COMPLEX); :: thesis: (multcomplexcpfunc A) . (a,((multcomplexcpfunc A) . (b,f))) = (multcomplexcpfunc A) . ((a * b),f)
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) . (b,f) as Element of PFuncs (A,COMPLEX) ;
reconsider h = (multcomplexcpfunc A) . (a,g) as Element of PFuncs (A,COMPLEX) ;
reconsider k = (multcomplexcpfunc A) . (c,f) as Element of PFuncs (A,COMPLEX) ;
A1: dom h = dom g by Th7;
A2: dom g = dom f by Th7;

A3: now :: thesis: for x being Element of A st x in dom h holds
h . x = k . x

let x be Element of A; :: thesis: ( x in dom h implies h . x = k . x )
assume A4: x in dom h ; :: thesis: h . x = k . x
hence h . x = a * (g . x) by A1, Th7
.= a * (b * (f . x)) by A2, A1, A4, Th7
.= (a * b) * (f . x)
.= k . x by A2, A1, A4, Th7 ;
:: thesis: verum

end;

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