theorem Th18: :: ALGSPEC1:18

for X, Y being set
for f being Function holds (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f)