theorem Th17: :: ALGSPEC1:17

for X, Y being set
for f being Function st X c= Y holds
(Y -indexing f) | X = X -indexing f