let Y be set ; :: thesis: for f being Function holds Y | f = f | (f " Y)
let f be Function; :: thesis: Y | f = f | (f " Y)
let x, y be set ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in Y | f or [x,y] in f | (f " Y) ) & ( not [x,y] in f | (f " Y) or [x,y] in Y | f ) )
thus ( [x,y] in Y | f implies [x,y] in f | (f " Y) ) :: thesis: ( not [x,y] in f | (f " Y) or [x,y] in Y | f )

proof

assume A1: [x,y] in Y | f ; :: thesis: [x,y] in f | (f " Y)
then A2: y in Y by RELAT_1:def 12;
A3: [x,y] in f by A1, RELAT_1:def 12;
then A4: x in dom f by FUNCT_1:8;
f . x in Y by A2, A3, FUNCT_1:8;
then x in f " Y by A4, FUNCT_1:def 13;
hence [x,y] in f | (f " Y) by A3, RELAT_1:def 11; :: thesis: verum

end;

assume A5: [x,y] in f | (f " Y) ; :: thesis: [x,y] in Y | f
then A6: x in f " Y by RELAT_1:def 11;
A7: [x,y] in f by A5, RELAT_1:def 11;
f . x in Y by A6, FUNCT_1:def 13;
then y in Y by A7, FUNCT_1:8;
hence [x,y] in Y | f by A7, RELAT_1:def 12; :: thesis: verum