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 l = dom ((multpfunc A) . f,g) ) by Th15;
A3: ( dom ((multpfunc A) . i,g) = (dom i) /\ (dom g) & dom ((multpfunc A) . f,g) = (dom f) /\ (dom g) ) by Th11;

now

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

end;

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