theorem :: FUNCOP_1:75

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