let f be Function; :: thesis: for Y1, Y2 being set st Y2 c= Y1 holds
(Y1 |` f) " Y2 = f " Y2
let Y1, Y2 be set ; :: thesis: ( Y2 c= Y1 implies (Y1 |` f) " Y2 = f " Y2 )
assume A1: Y2 c= Y1 ; :: thesis: (Y1 |` f) " Y2 = f " Y2
for x being object holds
( x in (Y1 |` f) " Y2 iff x in f " Y2 )

proof

let x be object ; :: thesis: ( x in (Y1 |` f) " Y2 iff x in f " Y2 )

hereby :: thesis: ( x in f " Y2 implies x in (Y1 |` f) " Y2 )

assume x in (Y1 |` f) " Y2 ; :: thesis: x in f " Y2
then consider y being object such that
A2: ( [x,y] in Y1 |` f & y in Y2 ) by RELAT_1:def 14;
[x,y] in f by A2, RELAT_1:def 12;
hence x in f " Y2 by A2, RELAT_1:def 14; :: thesis: verum

end;

assume x in f " Y2 ; :: thesis: x in (Y1 |` f) " Y2
then consider y being object such that
A3: ( [x,y] in f & y in Y2 ) by RELAT_1:def 14;
[x,y] in Y1 |` f by A3, A1, RELAT_1:def 12;
hence x in (Y1 |` f) " Y2 by A3, RELAT_1:def 14; :: thesis: verum

end;

hence (Y1 |` f) " Y2 = f " Y2 by TARSKI:2; :: thesis: verum