let Y, X 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:88, RELAT_1:117;
then (Y | f) | X c= f by XBOOLE_1:1;
hence (Y | f) | X tolerates f by Th131; :: thesis: verum