let R be Relation of X,Y; :: thesis: ( R is X -defined & R is Y -valued )
thus dom R c= X :: according to RELAT_1:def 18 :: thesis: R is Y -valued

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom R or x in X )
assume x in dom R ; :: thesis: x in X
then ex y being set st [x,y] in R by RELAT_1:def 4;
hence x in X by ZFMISC_1:87; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in proj2 R or y in Y )
assume y in rng R ; :: thesis: y in Y
then ex x being set st [x,y] in R by RELAT_1:def 5;
hence y in Y by ZFMISC_1:87; :: thesis: verum