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