let A be non empty set ; :: thesis: 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); :: thesis: (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 :: thesis: 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)) . x

let x be Element of A; :: thesis: ( 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)))) ; :: thesis: ((multpfunc A) . (f,((multpfunc A) . (g,h)))) . x = ((multpfunc A) . (((multpfunc A) . (f,g)),h)) . x
then 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 ; :: thesis: 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; :: thesis: verum