let f be Function; :: thesis: for Y being set holds dom (Y |` f) = f " Y

let Y be set ; :: thesis: dom (Y |` f) = f " Y

for x being object holds

( x in dom (Y |` f) iff x in f " Y )

let Y be set ; :: thesis: dom (Y |` f) = f " Y

for x being object holds

( x in dom (Y |` f) iff x in f " Y )

proof

hence
dom (Y |` f) = f " Y
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in dom (Y |` f) iff x in f " Y )

then consider y being object such that

A2: ( [x,y] in f & y in Y ) by RELAT_1:def 14;

[x,y] in Y |` f by A2, RELAT_1:def 12;

hence x in dom (Y |` f) by XTUPLE_0:def 12; :: thesis: verum

end;hereby :: thesis: ( x in f " Y implies x in dom (Y |` f) )

assume
x in f " Y
; :: thesis: x in dom (Y |` f)assume
x in dom (Y |` f)
; :: thesis: x in f " Y

then consider y being object such that

A1: [x,y] in Y |` f by XTUPLE_0:def 12;

( y in Y & [x,y] in f ) by A1, RELAT_1:def 12;

hence x in f " Y by RELAT_1:def 14; :: thesis: verum

end;then consider y being object such that

A1: [x,y] in Y |` f by XTUPLE_0:def 12;

( y in Y & [x,y] in f ) by A1, RELAT_1:def 12;

hence x in f " Y by RELAT_1:def 14; :: thesis: verum

then consider y being object such that

A2: ( [x,y] in f & y in Y ) by RELAT_1:def 14;

[x,y] in Y |` f by A2, RELAT_1:def 12;

hence x in dom (Y |` f) by XTUPLE_0:def 12; :: thesis: verum