theorem :: ALGSPEC1:14

for X being set holds X -indexing {} = id X ;