let a, x, y, z be object ; :: thesis: (a,a,a) --> (x,y,z) = a .--> z
thus (a,a,a) --> (x,y,z) = (a,a) --> (y,z) by Th81
.= a .--> z by Th81 ; :: thesis: verum