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 object ; :: 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 object st [x,y] in R by XTUPLE_0:def 12;
hence x in X by ZFMISC_1:87; :: thesis: verum

end;

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