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