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;
A2: ( dom ((multpfunc A) . f,((multpfunc A) . g,h)) = (dom f) /\ (dom ((multpfunc A) . g,h)) & dom ((multpfunc A) . ((multpfunc A) . f,g),h) = (dom ((multpfunc A) . f,g)) /\ (dom h) ) by Th11;
then A3: ( dom ((multpfunc A) . f,((multpfunc A) . g,h)) = (dom f) /\ ((dom g) /\ (dom h)) & dom ((multpfunc A) . ((multpfunc A) . f,g),h) = ((dom f) /\ (dom g)) /\ (dom h) ) by Th11;
A6: ( dom ((multpfunc A) . f,((multpfunc A) . g,h)) c= dom ((multpfunc A) . g,h) & dom ((multpfunc A) . ((multpfunc A) . f,g),h) c= dom ((multpfunc A) . f,g) ) by A2, 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 A8: 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
A11: x in dom ((multpfunc A) . ((multpfunc A) . f,g),h) by A3, A8, XBOOLE_1:16;
thus ((multpfunc A) . f,((multpfunc A) . g,h)) . x = (f . x) * (((multpfunc A) . g,h) . x) by Th11, A8
.= (f . x) * ((g . x) * (h . x)) by Th11, A6, A8
.= ((f . x) * (g . x)) * (h . x)
.= (((multpfunc A) . f,g) . x) * (h . x) by Th11, A6, A11
.= ((multpfunc A) . ((multpfunc A) . f,g),h) . x by Th11, A11 ; :: thesis: verum

end;

hence (multpfunc A) . f,((multpfunc A) . g,h) = (multpfunc A) . ((multpfunc A) . f,g),h by A3, PARTFUN1:34, XBOOLE_1:16; :: thesis: verum