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 i = (multrealpfunc A) . a,f as Element of PFuncs A,REAL ;
set j = (multpfunc A) . f,g;
set k = (multpfunc A) . i,g;
reconsider l = (multrealpfunc A) . a,((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

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:34; :: thesis: verum