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