theorem :: FUNCOP_1:74

for x, y being object holds x in dom (x .--> y)