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 f) /\ (dom g)) /\ (dom h) = (dom f) /\ ((dom g) /\ (dom h)) by XBOOLE_1:16;
( dom ((multpfunc A) . (f,h)) = (dom f) /\ (dom h) & dom ((multpfunc A) . (f,g)) = (dom f) /\ (dom g) ) by Th7;
then dom ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) = ((dom h) /\ (dom f)) /\ ((dom f) /\ (dom g)) by Th6;
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 A2: dom ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) = (dom h) /\ (((dom f) /\ (dom f)) /\ (dom g)) by XBOOLE_1:16;
A3: ((dom f) /\ (dom g)) /\ (dom h) = (dom g) /\ ((dom f) /\ (dom h)) by XBOOLE_1:16;

A4: now :: thesis: for x being Element of A st x in dom ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) holds
((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) . x = ((multpfunc A) . (f,((addpfunc A) . (g,h)))) . x

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 A5: 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) by A2, XBOOLE_0:def 4;
then A6: x in dom (f (#) g) by VALUED_1:def 4;
x in (dom g) /\ (dom h) by A2, A1, A5, XBOOLE_0:def 4;
then A7: x in dom (g + h) by VALUED_1:def 1;
((multpfunc A) . (f,g)) . x = (f (#) g) . x by Def3;
then A8: ((multpfunc A) . (f,g)) . x = (f . x) * (g . x) by A6, VALUED_1:def 4;
x in (dom f) /\ (dom h) by A2, A3, A5, XBOOLE_0:def 4;
then A9: x in dom (f (#) h) by VALUED_1:def 4;
((multpfunc A) . (f,h)) . x = (f (#) h) . x by Def3;
then A10: ((multpfunc A) . (f,h)) . x = (f . x) * (h . x) by A9, VALUED_1:def 4;
((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) . x = (((multpfunc A) . (f,g)) . x) + (((multpfunc A) . (f,h)) . x) by A5, Th6;
then ( ((addpfunc A) . (g,h)) . x = (g + h) . x & ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) . x = (f . x) * ((g . x) + (h . x)) ) by A8, A10, RFUNCT_3:def 4;
then A11: ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) . x = (f . x) * (((addpfunc A) . (g,h)) . x) by A7, VALUED_1:def 1;
x in (dom f) /\ (dom ((addpfunc A) . (g,h))) by A2, A1, A5, Th6;
then A12: x in dom (f (#) ((addpfunc A) . (g,h))) by VALUED_1:def 4;
((multpfunc A) . (f,((addpfunc A) . (g,h)))) . x = (f (#) ((addpfunc A) . (g,h))) . x by Def3;
hence ((addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))) . x = ((multpfunc A) . (f,((addpfunc A) . (g,h)))) . x by A12, A11, VALUED_1:def 4; :: thesis: verum

end;

( dom ((multpfunc A) . (f,((addpfunc A) . (g,h)))) = (dom f) /\ (dom ((addpfunc A) . (g,h))) & dom ((addpfunc A) . (g,h)) = (dom g) /\ (dom h) ) by Th6, Th7;
hence (multpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h))) by A2, A4, PARTFUN1:5, XBOOLE_1:16; :: thesis: verum