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