theorem Th5: :: LPSPACC1:5

for A being non empty set
for f, g, h being Element of PFuncs (A,COMPLEX) holds
( h = (multcpfunc A) . (f,g) iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ) ) )