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