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