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