for x, y being object holds x in dom (x .--> y) by TARSKI:def 1;