let a, x, y, z be set ; :: thesis: (a,a,a) --> (x,y,z) = a .--> z
thus (a,a,a) --> (x,y,z) = (a,a) --> (y,z) by FUNCT_4:81
.= a .--> z by FUNCT_4:81 ; :: thesis: verum