theorem Th20: :: ALGSPEC1:20

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