the carrier of X1 c= the carrier of X0 by A1, TSEP_1:4;
hence g | the carrier of X1 is Function of X1,Y by FUNCT_2:32; :: thesis: verum