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 Th50, RELAT_1:36;
hence ( ( dom f c= X or dom (g * f) c= X ) implies compose (<*f,g*>,X) = g * f ) by RELAT_1:51; :: thesis: verum