let y, z, w be Real; :: thesis: (((cosh (2 * y)) + (cosh (2 * z))) + (cosh (2 * w))) + (cosh (2 * ((y + z) + w))) = ((4 * (cosh (z + w))) * (cosh (w + y))) * (cosh (y + z))
(((cosh (2 * y)) + (cosh (2 * z))) + (cosh (2 * w))) + (cosh (2 * ((y + z) + w))) = 2 * (((1 / 2) * ((cosh (2 * ((y + z) + w))) + (cosh (2 * y)))) + ((1 / 2) * ((cosh (2 * w)) + (cosh (2 * z)))))
.= 2 * (((1 / 2) * ((2 * (cosh (((2 * ((y + z) + w)) / 2) + ((2 * y) / 2)))) * (cosh (((2 * ((y + z) + w)) / 2) - ((2 * y) / 2))))) + ((1 / 2) * ((cosh (2 * w)) + (cosh (2 * z))))) by Lm11
.= 2 * (((cosh (z + w)) * (cosh (((y + z) + w) + y))) + ((1 / 2) * ((2 * (cosh (((2 * w) / 2) + ((2 * z) / 2)))) * (cosh (((2 * w) / 2) - ((2 * z) / 2)))))) by Lm11
.= 2 * ((cosh (z + w)) * ((cosh ((2 * y) + (z + w))) + (cosh (w - z))))
.= 2 * ((cosh (z + w)) * ((2 * (cosh ((((2 * y) + (z + w)) / 2) + ((w - z) / 2)))) * (cosh ((((2 * y) + (z + w)) / 2) - ((w - z) / 2))))) by Lm11
.= ((4 * (cosh (z + w))) * (cosh (w + y))) * (cosh (y + z)) ;
hence (((cosh (2 * y)) + (cosh (2 * z))) + (cosh (2 * w))) + (cosh (2 * ((y + z) + w))) = ((4 * (cosh (z + w))) * (cosh (w + y))) * (cosh (y + z)) ; :: thesis: verum