let a, b, c be set ; :: thesis: (a,b .--> c) . a,b = c
[a,b] in {[a,b]} by TARSKI:def 1;
hence (a,b .--> c) . a,b = c by Th13; :: thesis: verum