let A be non empty set ; :: thesis:
let f, g, h be Element of PFuncs (A,COMPLEX); :: thesis:
set k = (multcpfunc A) . (f,g);

end;

assume that
A3: dom h = (dom f) /\ (dom g) and
A4: for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ; :: thesis:

let x be Element of A; :: thesis:
A6: ((multcpfunc A) . (f,g)) . x = (f (#) g) . x by Def3;
assume A7: x in dom h ; :: thesis:
then x in dom (f (#) g) by A3, VALUED_1:def 4;
hence ((multcpfunc A) . (f,g)) . x = (f . x) * (g . x) by A6, VALUED_1:def 4
.= h . x by A4, A7 ;
:: thesis:

end;