let a, b, x, y, z be object ; :: 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 Th14
.= (a,b) --> (x,z) by Th81 ; :: thesis: verum