let X be set ; for f, g, h being Function st ( dom f c= X or dom (g * f) c= X or dom ((h * g) * f) c= X ) holds
compose (<*f,g,h*>,X) = (h * g) * f
let f, g, h be Function; ( ( dom f c= X or dom (g * f) c= X or dom ((h * g) * f) c= X ) implies compose (<*f,g,h*>,X) = (h * g) * f )
A1:
( (h * g) * (f * (id X)) = h * (g * (f * (id X))) & g * (f * (id X)) = (g * f) * (id X) )
by RELAT_1:36;
A2:
h * (g * f) = (h * g) * f
by RELAT_1:36;
( compose (<*f,g,h*>,X) = ((h * g) * f) * (id X) & ((h * g) * f) * (id X) = (h * g) * (f * (id X)) )
by Th53, RELAT_1:36;
hence
( ( dom f c= X or dom (g * f) c= X or dom ((h * g) * f) c= X ) implies compose (<*f,g,h*>,X) = (h * g) * f )
by A1, A2, RELAT_1:51; verum