let X be set ; :: thesis: for f being Function holds f | X tolerates f
let f be Function; :: thesis: f | X tolerates f
f | X c= f by RELAT_1:59;
hence f | X tolerates f by Th52; :: thesis: verum