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