let x, y be set ; :: thesis: for A being set st x <> y holds
not x in rng ((id A) +* (x .--> y))
let A be set ; :: thesis: ( x <> y implies not x in rng ((id A) +* (x .--> y)) )
assume x <> y ; :: thesis: not x in rng ((id A) +* (x .--> y))
then not y in {x} by TARSKI:def 1;
then {x} misses rng ((id A) +* ({x} --> y)) by Th12;
hence not x in rng ((id A) +* (x .--> y)) by ZFMISC_1:48; :: thesis: verum