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) . (jj,f) as Element of PFuncs (A,REAL) ;

A1: now :: thesis: for x being Element of A st x in dom f holds
g . x = f . x

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:5; :: thesis: verum