let a be Real; :: thesis: for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (a,g))) = (multrealpfunc A) . (a,((addpfunc A) . (f,g)))
let A be non empty set ; :: thesis: for f, g being Element of PFuncs (A,REAL) holds (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (a,g))) = (multrealpfunc A) . (a,((addpfunc A) . (f,g)))
let f, g be Element of PFuncs (A,REAL); :: thesis: (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (a,g))) = (multrealpfunc A) . (a,((addpfunc A) . (f,g)))
reconsider aa = a as Element of REAL by XREAL_0:def 1;
reconsider h = (multrealpfunc A) . (aa,f) as Element of PFuncs (A,REAL) ;
reconsider i = (multrealpfunc A) . (aa,g) as Element of PFuncs (A,REAL) ;
set j = (addpfunc A) . (f,g);
reconsider k = (multrealpfunc A) . (aa,((addpfunc A) . (f,g))) as Element of PFuncs (A,REAL) ;
set l = (addpfunc A) . (h,i);
A1: ( dom h = dom f & dom i = dom g ) by Th9;
A2: dom ((addpfunc A) . (h,i)) = (dom h) /\ (dom i) by Th6;
A3: dom ((addpfunc A) . (f,g)) = (dom f) /\ (dom g) by Th6;

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

let x be Element of A; :: thesis: ( x in dom ((addpfunc A) . (h,i)) implies ((addpfunc A) . (h,i)) . x = k . x )
A5: h . x = (a (#) f) . x by Def4;
assume A6: x in dom ((addpfunc A) . (h,i)) ; :: thesis: ((addpfunc A) . (h,i)) . x = k . x
then A7: x in dom (f + g) by A1, A2, VALUED_1:def 1;
A8: i . x = (a (#) g) . x by Def4;
x in dom i by A2, A6, XBOOLE_0:def 4;
then x in dom g by Th9;
then x in dom (a (#) g) by VALUED_1:def 5;
then A9: i . x = a * (g . x) by A8, VALUED_1:def 5;
x in dom h by A2, A6, XBOOLE_0:def 4;
then x in dom f by Th9;
then x in dom (a (#) f) by VALUED_1:def 5;
then A10: h . x = a * (f . x) by A5, VALUED_1:def 5;
thus ((addpfunc A) . (h,i)) . x = (h . x) + (i . x) by A6, Th6
.= a * ((f . x) + (g . x)) by A10, A9
.= a * ((f + g) . x) by A7, VALUED_1:def 1
.= a * (((addpfunc A) . (f,g)) . x) by RFUNCT_3:def 4
.= k . x by A1, A3, A2, A6, Th9 ; :: thesis: verum

end;

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