let A be non empty set ; :: thesis: for f, g, h being Element of PFuncs A,REAL holds (multpfunc A) . f,((addpfunc A) . g,h) = (addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)
let f, g, h be Element of PFuncs A,REAL ; :: thesis: (multpfunc A) . f,((addpfunc A) . g,h) = (addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)
set i = (multpfunc A) . f,h;
set j = (multpfunc A) . f,g;
set k = (addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h);
set l = (addpfunc A) . g,h;
set m = (multpfunc A) . f,((addpfunc A) . g,h);
A1: ( dom ((multpfunc A) . f,h) = (dom f) /\ (dom h) & dom ((multpfunc A) . f,g) = (dom f) /\ (dom g) & dom ((multpfunc A) . f,((addpfunc A) . g,h)) = (dom f) /\ (dom ((addpfunc A) . g,h)) ) by Th11;
A2: ( dom ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) = (dom ((multpfunc A) . f,g)) /\ (dom ((multpfunc A) . f,h)) & dom ((addpfunc A) . g,h) = (dom g) /\ (dom h) ) by Th10;
dom ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) = ((dom h) /\ (dom f)) /\ ((dom f) /\ (dom g)) by A1, Th10;
then dom ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) = (dom h) /\ ((dom f) /\ ((dom f) /\ (dom g))) by XBOOLE_1:16;
then A3: dom ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) = (dom h) /\ (((dom f) /\ (dom f)) /\ (dom g)) by XBOOLE_1:16;
A6: ( ((dom f) /\ (dom g)) /\ (dom h) = (dom f) /\ ((dom g) /\ (dom h)) & ((dom f) /\ (dom g)) /\ (dom h) = (dom g) /\ ((dom f) /\ (dom h)) ) by XBOOLE_1:16;

now

let x be Element of A; :: thesis: ( x in dom ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) implies ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) . x = ((multpfunc A) . f,((addpfunc A) . g,h)) . x )
assume A14: x in dom ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) ; :: thesis: ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) . x = ((multpfunc A) . f,((addpfunc A) . g,h)) . x
then ( x in (dom f) /\ (dom g) & x in (dom f) /\ (dom h) & x in (dom g) /\ (dom h) & x in (dom f) /\ (dom ((addpfunc A) . g,h)) ) by A3, A6, Th10, XBOOLE_0:def 4;
then B1: ( x in dom (f (#) g) & x in dom (f (#) h) & x in dom (g + h) & x in dom (f (#) ((addpfunc A) . g,h)) ) by VALUED_1:def 1, VALUED_1:def 4;
( ((multpfunc A) . f,g) . x = (f (#) g) . x & ((multpfunc A) . f,h) . x = (f (#) h) . x ) by Def3;
then A22: ( ((multpfunc A) . f,g) . x = (f . x) * (g . x) & ((multpfunc A) . f,h) . x = (f . x) * (h . x) ) by B1, VALUED_1:def 4;
A24: ((addpfunc A) . g,h) . x = (g + h) . x by RFUNCT_3:def 4;
A25: ((multpfunc A) . f,((addpfunc A) . g,h)) . x = (f (#) ((addpfunc A) . g,h)) . x by Def3;
((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) . x = (((multpfunc A) . f,g) . x) + (((multpfunc A) . f,h) . x) by Th10, A14;
then ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) . x = (f . x) * ((g . x) + (h . x)) by A22;
then ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) . x = (f . x) * (((addpfunc A) . g,h) . x) by A24, B1, VALUED_1:def 1;
hence ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) . x = ((multpfunc A) . f,((addpfunc A) . g,h)) . x by A25, B1, VALUED_1:def 4; :: thesis: verum

end;

hence (multpfunc A) . f,((addpfunc A) . g,h) = (addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h) by A3, A1, A2, PARTFUN1:34, XBOOLE_1:16; :: thesis: verum