let A be non empty set ; :: thesis: for f, g, h being Element of PFuncs (A,COMPLEX) holds (multcpfunc A) . (f,((addcpfunc A) . (g,h))) = (addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))
let f, g, h be Element of PFuncs (A,COMPLEX); :: thesis: (multcpfunc A) . (f,((addcpfunc A) . (g,h))) = (addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))
set i = (multcpfunc A) . (f,h);
set j = (multcpfunc A) . (f,g);
set k = (addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)));
set l = (addcpfunc A) . (g,h);
set m = (multcpfunc A) . (f,((addcpfunc A) . (g,h)));
A1: ((dom f) /\ (dom g)) /\ (dom h) = (dom f) /\ ((dom g) /\ (dom h)) by XBOOLE_1:16;
( dom ((multcpfunc A) . (f,h)) = (dom f) /\ (dom h) & dom ((multcpfunc A) . (f,g)) = (dom f) /\ (dom g) ) by Th5;
then dom ((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) = ((dom h) /\ (dom f)) /\ ((dom f) /\ (dom g)) by Th4;
then dom ((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) = (dom h) /\ ((dom f) /\ ((dom f) /\ (dom g))) by XBOOLE_1:16;
then A2: dom ((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc 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 ((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) holds
((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) . x = ((multcpfunc A) . (f,((addcpfunc A) . (g,h)))) . x

let x be Element of A; :: thesis: ( x in dom ((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) implies ((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) . x = ((multcpfunc A) . (f,((addcpfunc A) . (g,h)))) . x )
assume A5: x in dom ((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) ; :: thesis: ((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) . x = ((multcpfunc A) . (f,((addcpfunc 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;
((multcpfunc A) . (f,g)) . x = (f (#) g) . x by Def3;
then A8: ((multcpfunc 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;
((multcpfunc A) . (f,h)) . x = (f (#) h) . x by Def3;
then A10: ((multcpfunc A) . (f,h)) . x = (f . x) * (h . x) by A9, VALUED_1:def 4;
((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) . x = (((multcpfunc A) . (f,g)) . x) + (((multcpfunc A) . (f,h)) . x) by A5, Th4;
then ( ((addcpfunc A) . (g,h)) . x = (g + h) . x & ((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) . x = (f . x) * ((g . x) + (h . x)) ) by A8, A10, Def5;
then A11: ((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) . x = (f . x) * (((addcpfunc A) . (g,h)) . x) by A7, VALUED_1:def 1;
x in (dom f) /\ (dom ((addcpfunc A) . (g,h))) by A2, A1, A5, Th4;
then A12: x in dom (f (#) ((addcpfunc A) . (g,h))) by VALUED_1:def 4;
((multcpfunc A) . (f,((addcpfunc A) . (g,h)))) . x = (f (#) ((addcpfunc A) . (g,h))) . x by Def3;
hence ((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) . x = ((multcpfunc A) . (f,((addcpfunc A) . (g,h)))) . x by A12, A11, VALUED_1:def 4; :: thesis: verum

end;

( dom ((multcpfunc A) . (f,((addcpfunc A) . (g,h)))) = (dom f) /\ (dom ((addcpfunc A) . (g,h))) & dom ((addcpfunc A) . (g,h)) = (dom g) /\ (dom h) ) by Th4, Th5;
hence (multcpfunc A) . (f,((addcpfunc A) . (g,h))) = (addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h))) by A2, A4, PARTFUN1:5, XBOOLE_1:16; :: thesis: verum