for X being set
for f being Function holds X -indexing ((id X) +* f) = X -indexing f