the carrier of X0 c= the carrier of X by BORSUK_1:35;
hence f | the carrier of X0 is Function of X0,Y by FUNCT_2:38; :: thesis: verum