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 Th11;
then dom ((multpfunc A) . (RealPFuncUnit A),f) = A /\ (dom f) by FUNCOP_1:19;
then A4: dom ((multpfunc A) . (RealPFuncUnit A),f) = dom f by XBOOLE_1:28;

now

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 A4, Th11;
then ((multpfunc A) . (RealPFuncUnit A),f) . x = 1 * (f . x) by FUNCOP_1:13;
hence ((multpfunc A) . (RealPFuncUnit A),f) . x = f . x ; :: thesis: verum

end;

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