let Y, X be set ; :: thesis: for R being Relation of X,Y holds
( ( for x being set st x in X holds
ex y being set st [x,y] in R ) iff dom R = X )
let R be Relation of X,Y; :: thesis: ( ( for x being set st x in X holds
ex y being set st [x,y] in R ) iff dom R = X )
thus ( ( for x being set st x in X holds
ex y being set st [x,y] in R ) implies dom R = X ) :: thesis: ( dom R = X implies for x being set st x in X holds
ex y being set st [x,y] in R )

proof

assume A1: for x being set st x in X holds
ex y being set st [x,y] in R ; :: thesis: dom R = X
thus dom R = X :: thesis: verum

proof

now

let x be set ; :: thesis: ( x in dom R iff x in X )

now

assume x in X ; :: thesis: x in dom R
then ex y being set st [x,y] in R by A1;
hence x in dom R by RELAT_1:20; :: thesis: verum

end;

hence ( x in dom R iff x in X ) ; :: thesis: verum

end;

hence dom R = X by TARSKI:2; :: thesis: verum

end;

end;

thus ( dom R = X implies for x being set st x in X holds
ex y being set st [x,y] in R ) by RELAT_1:def 4; :: thesis: verum