let a, b be Real; :: thesis: for A being non empty set
for f being Element of PFuncs A,REAL holds (addpfunc A) . ((multrealpfunc A) . a,f),((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 (addpfunc A) . ((multrealpfunc A) . a,f),((multrealpfunc A) . b,f) = (multrealpfunc A) . (a + b),f
let f be Element of PFuncs A,REAL ; :: thesis: (addpfunc A) . ((multrealpfunc A) . a,f),((multrealpfunc A) . b,f) = (multrealpfunc A) . (a + b),f
reconsider g = (multrealpfunc A) . a,f as Element of PFuncs A,REAL ;
reconsider h = (multrealpfunc A) . b,f as Element of PFuncs A,REAL ;
reconsider k = (multrealpfunc A) . (a + b),f as Element of PFuncs A,REAL ;
set j = (addpfunc A) . g,h;
A1: ( dom g = dom f & dom h = dom f & dom k = dom f ) by Th15;
then (dom h) /\ (dom g) = (dom f) /\ (dom f) ;
then A3: dom ((addpfunc A) . g,h) = dom f by Th10;

now

let x be Element of A; :: thesis: ( x in dom ((addpfunc A) . g,h) implies ((addpfunc A) . g,h) . x = k . x )
assume A5: x in dom ((addpfunc A) . g,h) ; :: thesis: ((addpfunc A) . g,h) . x = k . x
then ( x in dom (a (#) f) & x in dom (b (#) f) ) by A3, VALUED_1:def 5;
then ( (a (#) f) . x = a * (f . x) & (b (#) f) . x = b * (f . x) ) by VALUED_1:def 5;
then ( g . x = a * (f . x) & h . x = b * (f . x) ) by Def4;
then (g . x) + (h . x) = (a + b) * (f . x) ;
hence ((addpfunc A) . g,h) . x = (a + b) * (f . x) by Th10, A5
.= k . x by Th15, A3, A5 ;
:: thesis: verum

end;

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