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 aa = a, bb = b as Element of REAL by XREAL_0:def 1;
reconsider g = (multrealpfunc A) . (aa,f) as Element of PFuncs (A,REAL) ;
reconsider h = (multrealpfunc A) . (bb,f) as Element of PFuncs (A,REAL) ;
reconsider k = (multrealpfunc A) . ((aa + bb),f) as Element of PFuncs (A,REAL) ;
set j = (addpfunc A) . (g,h);
dom g = dom f by Th9;
then (dom h) /\ (dom g) = (dom f) /\ (dom f) by Th9;
then A1: dom ((addpfunc A) . (g,h)) = dom f by Th6;

A2: now :: thesis: for x being Element of A st x in dom ((addpfunc A) . (g,h)) holds
((addpfunc A) . (g,h)) . x = k . x

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

end;

dom k = dom f by Th9;
hence (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a + b),f) by A1, A2, PARTFUN1:5; :: thesis: verum