theorem Th7: :: LPSPACE1:7

for A being non empty set
for f, g, h being Element of PFuncs (A,REAL) holds
( h = (multpfunc 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) ) ) )