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