for X, Y being non empty set
for f being Function of X,Y holds [:f,f:] " (id Y) is Equivalence_Relation of X