let X, Y be set ; :: thesis: for f being Function holds (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f)
let f be Function; :: thesis: (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f)
A1: X -indexing f tolerates Y -indexing f by Th19;
(X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f) by Th18;
hence (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f) by A1, FUNCT_4:30; :: thesis: verum