theorem :: ALGSPEC1:15

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