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:55;
A2: h * (g * f) = (h * g) * f by RELAT_1:55;
( compose <*f,g,h*>,X = ((h * g) * f) * (id X) & ((h * g) * f) * (id X) = (h * g) * (f * (id X)) ) by Th56, RELAT_1:55;
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:77; :: thesis: verum