let A be non empty set ; :: thesis: for f being Element of PFuncs (A,REAL) holds (multpfunc A) . ((RealPFuncUnit A),f) = f
let f be Element of PFuncs (A,REAL); :: thesis: (multpfunc A) . ((RealPFuncUnit A),f) = f
set h = (multpfunc A) . ((RealPFuncUnit A),f);
dom ((multpfunc A) . ((RealPFuncUnit A),f)) = (dom (RealPFuncUnit A)) /\ (dom f) by Th7;
then dom ((multpfunc A) . ((RealPFuncUnit A),f)) = A /\ (dom f) by FUNCOP_1:13;
then A1: dom ((multpfunc A) . ((RealPFuncUnit A),f)) = dom f by XBOOLE_1:28;

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

let x be Element of A; :: thesis: ( x in dom f implies ((multpfunc A) . ((RealPFuncUnit A),f)) . x = f . x )
assume x in dom f ; :: thesis: ((multpfunc A) . ((RealPFuncUnit A),f)) . x = f . x
then ((multpfunc A) . ((RealPFuncUnit A),f)) . x = ((RealPFuncUnit A) . x) * (f . x) by A1, Th7;
then ((multpfunc A) . ((RealPFuncUnit A),f)) . x = 1 * (f . x) by FUNCOP_1:7;
hence ((multpfunc A) . ((RealPFuncUnit A),f)) . x = f . x ; :: thesis: verum

end;

hence (multpfunc A) . ((RealPFuncUnit A),f) = f by A1, PARTFUN1:5; :: thesis: verum