let A be non empty set ; :: thesis: for h, f, g 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 h, f, g 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) ) ) )

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 A2: 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 A5: x in dom (f (#) g) by A2, Def3;
h . x = (f (#) g) . x by A2, Def3;
hence h . x = (f . x) * (g . x) by A5, VALUED_1:def 4; :: thesis: verum

end;

assume A7: ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ) ) ; :: thesis: h = (multpfunc A) . f,g
set k = (multpfunc A) . f,g;

A8: now

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

end;

dom ((multpfunc A) . f,g) = dom (f (#) g) by Def3
.= dom h by A7, VALUED_1:def 4 ;
hence h = (multpfunc A) . f,g by A8, PARTFUN1:34; :: thesis: verum