( dom (id Y) = Y & rng (id Y) = Y ) ;
hence id Y is Function of Y,X by A1, FUNCT_2:2; :: thesis: verum