for X being set
for f being Function st f c= id X holds
X -indexing f = id X