take f = the empty one-to-one Function; :: thesis: ( f is empty & f is X -defined & f is Y -valued & f is one-to-one )

( dom f = {} & rng f = {} ) ;

hence ( f is empty & f is X -defined & f is Y -valued & f is one-to-one ) by RELAT_1:def 18, RELAT_1:def 19, XBOOLE_1:2; :: thesis: verum

( dom f = {} & rng f = {} ) ;

hence ( f is empty & f is X -defined & f is Y -valued & f is one-to-one ) by RELAT_1:def 18, RELAT_1:def 19, XBOOLE_1:2; :: thesis: verum