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