let A be non empty set ; :: thesis: 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) ) ) )
let f, g, h be Element of PFuncs (A,REAL); :: thesis: ( 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) ) ) )
set k = (multpfunc A) . (f,g);

hereby :: thesis: ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ) implies h = (multpfunc A) . (f,g) )

assume A1: h = (multpfunc A) . (f,g) ; :: thesis: ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ) )
hence dom h = dom (f (#) g) by Def3
.= (dom f) /\ (dom g) by VALUED_1:def 4 ;
:: thesis: for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x)
let x be Element of A; :: thesis: ( x in dom h implies h . x = (f . x) * (g . x) )
assume x in dom h ; :: thesis: h . x = (f . x) * (g . x)
then A2: x in dom (f (#) g) by A1, Def3;
h . x = (f (#) g) . x by A1, Def3;
hence h . x = (f . x) * (g . x) by A2, VALUED_1:def 4; :: thesis: verum

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: h = (multpfunc A) . (f,g)

A5: now :: thesis: for x being Element of A st x in dom h holds
((multpfunc A) . (f,g)) . x = h . x

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

end;

dom ((multpfunc A) . (f,g)) = dom (f (#) g) by Def3
.= dom h by A3, VALUED_1:def 4 ;
hence h = (multpfunc A) . (f,g) by A5, PARTFUN1:5; :: thesis: verum