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