let A be non empty set ; 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); (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 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)))) . xlet x be
Element of
A;
( 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))))
;
((addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (f,h)))) . x = ((multcpfunc A) . (f,((addcpfunc A) . (g,h)))) . xthen
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;
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; verum