( the carrier of Y <> {} & 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:38; :: thesis: verum