theorem :: ALGSPEC1:16

for f being Function holds {} -indexing f = {} ;