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 )

(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

hence
(Y1 |` f) " Y2 = f " Y2
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in (Y1 |` f) " Y2 iff x in 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;hereby :: thesis: ( x in f " Y2 implies x in (Y1 |` f) " Y2 )

assume
x in f " Y2
; :: thesis: x in (Y1 |` f) " Y2assume
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;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

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