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

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:34, XBOOLE_1:16; :: thesis: verum