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