let X, Y be set ; :: thesis: for f being Function holds X -indexing f tolerates Y -indexing f
let f be Function; :: thesis: X -indexing f tolerates Y -indexing f
Y -indexing f = ((X \/ Y) -indexing f) | Y by Th17, XBOOLE_1:7;
then A1: Y -indexing f c= (X \/ Y) -indexing f by RELAT_1:59;
X -indexing f = ((X \/ Y) -indexing f) | X by Th17, XBOOLE_1:7;
then X -indexing f c= (X \/ Y) -indexing f by RELAT_1:59;
hence X -indexing f tolerates Y -indexing f by A1, PARTFUN1:52; :: thesis: verum