theorem :: FUNCOP_1:74

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