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 h = (multrealpfunc A) . a,f as Element of PFuncs A,REAL ;
reconsider i = (multrealpfunc A) . a,g as Element of PFuncs A,REAL ;
set j = (addpfunc A) . f,g;
reconsider k = (multrealpfunc A) . a,((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 & dom k = dom ((addpfunc A) . f,g) ) by Th15;
A3: ( dom ((addpfunc A) . f,g) = (dom f) /\ (dom g) & dom ((addpfunc A) . h,i) = (dom h) /\ (dom i) ) by Th10;

now

let x be Element of A; :: thesis: ( x in dom ((addpfunc A) . h,i) implies ((addpfunc A) . h,i) . x = k . x )
assume A9: x in dom ((addpfunc A) . h,i) ; :: thesis: ((addpfunc A) . h,i) . x = k . x
then B2: x in dom (f + g) by A1, A3, VALUED_1:def 1;
( x in dom h & x in dom i ) by A9, A3, XBOOLE_0:def 4;
then ( x in dom f & x in dom g ) by Th15;
then A11: ( x in dom (a (#) f) & x in dom (a (#) g) ) by VALUED_1:def 5;
( h . x = (a (#) f) . x & i . x = (a (#) g) . x ) by Def4;
then A12: ( h . x = a * (f . x) & i . x = a * (g . x) ) by A11, VALUED_1:def 5;
thus ((addpfunc A) . h,i) . x = (h . x) + (i . x) by A9, Th10
.= a * ((f . x) + (g . x)) by A12
.= a * ((f + g) . x) by B2, VALUED_1:def 1
.= a * (((addpfunc A) . f,g) . x) by RFUNCT_3:def 4
.= k . x by A9, A1, A3, Th15 ; :: thesis: verum

end;

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