let y, z, w be Real; :: thesis: (((((sinh y) * (sinh z)) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) = 0
(((((sinh y) * (sinh z)) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) = (((((1 / 2) * ((cosh (y + z)) - (cosh (y - z)))) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11
.= ((((1 / 2) * (((cosh (y + z)) * (sinh (z - y))) - ((cosh (y - z)) * (sinh (z - y))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w)))
.= ((((1 / 2) * (((1 / 2) * ((sinh ((y + z) + (z - y))) - (sinh ((y + z) - (z - y))))) - ((cosh (y - z)) * (sinh (z - y))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11
.= ((((1 / 2) * (((1 / 2) * ((sinh (2 * z)) - (sinh (y + y)))) - ((1 / 2) * ((sinh ((y - z) + (- (y - z)))) - (sinh ((y - z) - (z - y))))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11
.= ((((1 / 2) * (((1 / 2) * ((sinh (2 * z)) - (sinh (2 * y)))) - ((1 / 2) * (() - (sinh (2 * (y - z))))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by SIN_COS2:def 2
.= ((((1 / 2) * ((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))))) + (((1 / 2) * ((cosh (z + w)) - (cosh (z - w)))) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by
.= (((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((cosh (z + w)) * (sinh (w - z))) - ((cosh (z - w)) * (sinh (w - z)))))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w)))
.= (((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh ((z + w) + (w - z))) - (sinh ((z + w) - (w - z))))) - ((cosh (z - w)) * (sinh (w - z)))))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11
.= (((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * ((sinh ((z - w) + (w - z))) - (sinh ((z - w) - (w - z)))))))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11
.= (((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * (0 - (sinh ((z - w) - (w - z)))))))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by
.= (((1 / 2) * ((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w)))))))) + (((1 / 2) * ((cosh (w + y)) - (cosh (w - y)))) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11
.= ((1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((cosh (w + y)) * (sinh (y - w))) - ((cosh (w - y)) * (sinh (y - w)))))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w)))
.= ((1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh ((w + y) + (y - w))) - (sinh ((w + y) - (y - w))))) - ((cosh (w - y)) * (sinh (y - w)))))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11
.= ((1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh (2 * y)) - (sinh (2 * w)))) - ((1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (- (w - y))))))))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by Th11
.= ((1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh (2 * y)) - (sinh (2 * w)))) - ((1 / 2) * (0 - (sinh (2 * (w - y)))))))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) by
.= ((1 / 2) * ((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y)))))) + (((1 / 2) * ((cosh ((z - y) + (- (z - w)))) - (cosh ((z - y) - (w - z))))) * (sinh (y - w))) by Th11
.= (1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((cosh (w - y)) * (sinh (y - w))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w)))))
.= (1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (y - w))))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w))))) by Th11
.= (1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((1 / 2) * (0 - (sinh ((w - y) - (y - w))))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w))))) by
.= (1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((1 / 2) * (- (sinh (2 * (w - y))))) - ((1 / 2) * ((sinh (((z - y) + (z - w)) + (y - w))) - (sinh (((z - y) + (z - w)) - (y - w))))))) by Th11
.= (1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + ((1 / 2) * (((sinh (- (2 * (y - z)))) - (sinh (2 * (z - w)))) + (- (sinh (2 * (w - y)))))))
.= (1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + ((1 / 2) * (((- (sinh (2 * (y - z)))) - (sinh (2 * (z - w)))) + (- (sinh (2 * (w - y))))))) by Lm8 ;
hence (((((sinh y) * (sinh z)) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) = 0 ; :: thesis: verum