let a, b be Real; for A being non empty set
for f being Element of PFuncs (A,REAL) holds (multrealpfunc A) . (a,((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a * b),f)
let A be non empty set ; for f being Element of PFuncs (A,REAL) holds (multrealpfunc A) . (a,((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a * b),f)
let f be Element of PFuncs (A,REAL); (multrealpfunc A) . (a,((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a * b),f)
reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;
reconsider g = (multrealpfunc A) . (bb,f) as Element of PFuncs (A,REAL) ;
reconsider h = (multrealpfunc A) . (aa,g) as Element of PFuncs (A,REAL) ;
reconsider k = (multrealpfunc A) . ((aa * bb),f) as Element of PFuncs (A,REAL) ;
A1:
dom h = dom g
by Th9;
A2:
dom g = dom f
by Th9;
dom k = dom f
by Th9;
hence
(multrealpfunc A) . (a,((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a * b),f)
by A2, A1, A3, PARTFUN1:5; verum