let A be non empty set ; :: thesis: for f being Element of PFuncs (A,REAL) holds (multrealpfunc A) . (1,f) = f
let f be Element of PFuncs (A,REAL); :: thesis: (multrealpfunc A) . (1,f) = f
reconsider g = (multrealpfunc A) . (1,f) as Element of PFuncs (A,REAL) ;

A1: now

let x be Element of A; :: thesis: ( x in dom f implies g . x = f . x )
assume x in dom f ; :: thesis: g . x = f . x
hence g . x = 1 * (f . x) by Th9
.= f . x ;
:: thesis: verum

end;

dom g = dom f by Th9;
hence (multrealpfunc A) . (1,f) = f by A1, PARTFUN1:34; :: thesis: verum