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

A3: now :: thesis: for x being Element of A st x in dom ((multpfunc A) . (i,g)) holds
((multpfunc A) . (i,g)) . x = l . x

let x be Element of A; :: thesis: ( x in dom ((multpfunc A) . (i,g)) implies ((multpfunc A) . (i,g)) . x = l . x )
A4: ((multpfunc A) . (f,g)) . x = (f (#) g) . x by Def3;
assume A5: x in dom ((multpfunc A) . (i,g)) ; :: thesis: ((multpfunc A) . (i,g)) . x = l . x
then x in dom (f (#) g) by A1, VALUED_1:def 4;
then A6: ((multpfunc A) . (f,g)) . x = (f . x) * (g . x) by A4, VALUED_1:def 4;
A7: ( i . x = (a (#) f) . x & dom (a (#) f) = dom f ) by Def4, VALUED_1:def 5;
x in dom f by A1, A5, XBOOLE_0:def 4;
then A8: i . x = a * (f . x) by A7, VALUED_1:def 5;
A9: l . x = (a (#) ((multpfunc A) . (f,g))) . x by Def4;
x in dom (a (#) ((multpfunc A) . (f,g))) by A1, A2, A5, VALUED_1:def 5;
then A10: l . x = a * ((f . x) * (g . x)) by A6, A9, VALUED_1:def 5;
((multpfunc A) . (i,g)) . x = (i . x) * (g . x) by A5, Th7;
hence ((multpfunc A) . (i,g)) . x = l . x by A8, A10; :: thesis: verum

end;

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