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