let A be non empty set ; for f, g, h being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,((multpfunc A) . (g,h))) = (multpfunc A) . (((multpfunc A) . (f,g)),h)
let f, g, h be Element of PFuncs (A,REAL); (multpfunc A) . (f,((multpfunc A) . (g,h))) = (multpfunc A) . (((multpfunc A) . (f,g)),h)
set j = (multpfunc A) . (g,h);
set k = (multpfunc A) . (f,g);
set j1 = (multpfunc A) . (f,((multpfunc A) . (g,h)));
set k1 = (multpfunc A) . (((multpfunc A) . (f,g)),h);
A1:
dom ((multpfunc A) . (((multpfunc A) . (f,g)),h)) = (dom ((multpfunc A) . (f,g))) /\ (dom h)
by Th7;
then A2:
dom ((multpfunc A) . (((multpfunc A) . (f,g)),h)) c= dom ((multpfunc A) . (f,g))
by XBOOLE_1:17;
A3:
dom ((multpfunc A) . (((multpfunc A) . (f,g)),h)) = ((dom f) /\ (dom g)) /\ (dom h)
by A1, Th7;
A4:
dom ((multpfunc A) . (f,((multpfunc A) . (g,h)))) = (dom f) /\ (dom ((multpfunc A) . (g,h)))
by Th7;
then A5:
dom ((multpfunc A) . (f,((multpfunc A) . (g,h)))) = (dom f) /\ ((dom g) /\ (dom h))
by Th7;
A6:
dom ((multpfunc A) . (f,((multpfunc A) . (g,h)))) c= dom ((multpfunc A) . (g,h))
by A4, XBOOLE_1:17;
now for x being Element of A st x in dom ((multpfunc A) . (f,((multpfunc A) . (g,h)))) holds
((multpfunc A) . (f,((multpfunc A) . (g,h)))) . x = ((multpfunc A) . (((multpfunc A) . (f,g)),h)) . xlet x be
Element of
A;
( x in dom ((multpfunc A) . (f,((multpfunc A) . (g,h)))) implies ((multpfunc A) . (f,((multpfunc A) . (g,h)))) . x = ((multpfunc A) . (((multpfunc A) . (f,g)),h)) . x )assume A7:
x in dom ((multpfunc A) . (f,((multpfunc A) . (g,h))))
;
((multpfunc A) . (f,((multpfunc A) . (g,h)))) . x = ((multpfunc A) . (((multpfunc A) . (f,g)),h)) . xthen A8:
x in dom ((multpfunc A) . (((multpfunc A) . (f,g)),h))
by A5, A3, XBOOLE_1:16;
thus ((multpfunc A) . (f,((multpfunc A) . (g,h)))) . x =
(f . x) * (((multpfunc A) . (g,h)) . x)
by A7, Th7
.=
(f . x) * ((g . x) * (h . x))
by A6, A7, Th7
.=
((f . x) * (g . x)) * (h . x)
.=
(((multpfunc A) . (f,g)) . x) * (h . x)
by A2, A8, Th7
.=
((multpfunc A) . (((multpfunc A) . (f,g)),h)) . x
by A8, Th7
;
verum end;
hence
(multpfunc A) . (f,((multpfunc A) . (g,h))) = (multpfunc A) . (((multpfunc A) . (f,g)),h)
by A5, A3, PARTFUN1:5, XBOOLE_1:16; verum