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 h = dom g by Th9;
A2: dom g = dom f by Th9;

A3: 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, Th9
.= a * (b * (f . x)) by A2, A1, A4, Th9
.= (a * b) * (f . x)
.= k . x by A2, A1, A4, Th9 ;
:: thesis: verum

end;

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