let F, G, H be Function-yielding Function; :: thesis: (H ** G) ** F = H ** (G ** F)
set f = (H ** G) ** F;
set g = H ** (G ** F);

now :: thesis: ( dom ((H ** G) ** F) = dom (H ** (G ** F)) & ( for x being object st x in dom ((H ** G) ** F) holds
((H ** G) ** F) . x = (H ** (G ** F)) . x ) )

A1: dom ((H ** G) ** F) = (dom (H ** G)) /\ (dom F) by Def19
.= ((dom H) /\ (dom G)) /\ (dom F) by Def19 ;
then A2: dom ((H ** G) ** F) = (dom H) /\ ((dom G) /\ (dom F)) by XBOOLE_1:16;
hence A3: dom ((H ** G) ** F) = (dom H) /\ (dom (G ** F)) by Def19
.= dom (H ** (G ** F)) by Def19 ;
:: thesis: for x being object st x in dom ((H ** G) ** F) holds
((H ** G) ** F) . x = (H ** (G ** F)) . x
let x be object ; :: thesis: ( x in dom ((H ** G) ** F) implies ((H ** G) ** F) . x = (H ** (G ** F)) . x )
assume A4: x in dom ((H ** G) ** F) ; :: thesis: ((H ** G) ** F) . x = (H ** (G ** F)) . x
then x in (dom H) /\ (dom G) by A1, XBOOLE_0:def 4;
then A5: x in dom (H ** G) by Def19;
x in (dom G) /\ (dom F) by A2, A4, XBOOLE_0:def 4;
then A6: x in dom (G ** F) by Def19;
thus ((H ** G) ** F) . x = ((H ** G) . x) * (F . x) by A4, Def19
.= ((H . x) * (G . x)) * (F . x) by A5, Def19
.= (H . x) * ((G . x) * (F . x)) by RELAT_1:36
.= (H . x) * ((G ** F) . x) by A6, Def19
.= (H ** (G ** F)) . x by A3, A4, Def19 ; :: thesis: verum

end;

hence (H ** G) ** F = H ** (G ** F) ; :: thesis: verum