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
( X -indexing f = ((X \/ Y) -indexing f) | X & Y -indexing f = ((X \/ Y) -indexing f) | Y ) by Th18, XBOOLE_1:7;
then ( X -indexing f c= (X \/ Y) -indexing f & Y -indexing f c= (X \/ Y) -indexing f ) by RELAT_1:88;
hence X -indexing f tolerates Y -indexing f by PARTFUN1:131; :: thesis: verum