let X, Y be set ; :: thesis: for f being Function holds (Y |` f) | X tolerates f
let f be Function; :: thesis: (Y |` f) | X tolerates f
( (Y |` f) | X c= Y |` f & Y |` f c= f ) by RELAT_1:59, RELAT_1:86;
then (Y |` f) | X c= f ;
hence (Y |` f) | X tolerates f by Th52; :: thesis: verum