let X be set ; :: thesis: 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; :: thesis: ( ( 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; :: thesis: verum