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