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)
( (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f) & X -indexing f tolerates Y -indexing f ) by Th19, Th20;
hence (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f) by FUNCT_4:31; :: thesis: verum