let A be non empty set ; :: thesis: for f being Element of PFuncs (A,COMPLEX) holds (multcomplexcpfunc A) . (1r,f) = f
let f be Element of PFuncs (A,COMPLEX); :: thesis: (multcomplexcpfunc A) . (1r,f) = f
reconsider g = (multcomplexcpfunc A) . (1r,f) as Element of PFuncs (A,COMPLEX) ;

A1: now :: thesis: for x being Element of A st x in dom f holds
g . x = f . x

let x be Element of A; :: thesis: ( x in dom f implies g . x = f . x )
assume x in dom f ; :: thesis: g . x = f . x
hence g . x = 1r * (f . x) by Th7
.= f . x by COMPLEX1:def 4 ;
:: thesis: verum

end;

dom g = dom f by Th7;
hence (multcomplexcpfunc A) . (1r,f) = f by A1, PARTFUN1:5; :: thesis: verum