theorem :: FUNCT_7:13

for x, y, A being set st x <> y holds
not x in rng ((id A) +* (x .--> y))