theorem Th19: :: ALGSPEC1:19

for X, Y being set
for f being Function holds X -indexing f tolerates Y -indexing f