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: dom g = dom f by Th15;

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 Th15
.= f . x ;
:: thesis: verum

end;

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