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

proof

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

now :: thesis: for x being object holds
( x in dom R iff x in X )

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

now :: thesis: ( x in X implies x in dom R )

assume x in X ; :: thesis: x in dom R
then ex y being object st [x,y] in R by A1;
hence x in dom R by XTUPLE_0:def 12; :: 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;

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