let z, x, y be set ; :: thesis: ( z in dom (x .--> y) implies z = x )
dom (x .--> y) = {x} by Th19;
hence ( z in dom (x .--> y) implies z = x ) by TARSKI:def 1; :: thesis: verum