theorem Th10: :: ALGSPEC1:10

for X being set
for f being Function st dom f = X holds
X -indexing f = f