:: deftheorem defines -indexing ALGSPEC1:def 1 :
for X being set
for f being Function holds X -indexing f = (id X) +* (f | X);