theorem Th7: :: LPSPACC1:7

for a being Complex
for A being non empty set
for f, h being Element of PFuncs (A,COMPLEX) holds
( h = (multcomplexcpfunc A) . (a,f) iff ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) ) )