let a, b be Real; :: thesis: 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 ; :: thesis: 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 ; :: thesis: (multrealpfunc A) . a,((multrealpfunc A) . b,f) = (multrealpfunc A) . (a * b),f
reconsider g = (multrealpfunc A) . b,f as Element of PFuncs A,REAL ;
reconsider h = (multrealpfunc A) . a,g as Element of PFuncs A,REAL ;
reconsider k = (multrealpfunc A) . (a * b),f as Element of PFuncs A,REAL ;
A1: ( dom g = dom f & dom h = dom g & dom k = dom f ) by Th15;

now

let x be Element of A; :: thesis: ( x in dom h implies h . x = k . x )
assume A4: x in dom h ; :: thesis: h . x = k . x
hence h . x = a * (g . x) by A1, Th15
.= a * (b * (f . x)) by A4, A1, Th15
.= (a * b) * (f . x)
.= k . x by A1, A4, Th15 ;
:: thesis: verum

end;

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