let x be Real; :: thesis: (((sinh (5 * x)) + (2 * (sinh (3 * x)))) + (sinh x)) / (((sinh (7 * x)) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) = (sinh (3 * x)) / (sinh (5 * x))
(((sinh (5 * x)) + (2 * (sinh (3 * x)))) + (sinh x)) / (((sinh (7 * x)) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) = (((sinh ((3 * x) + (2 * x))) + (2 * (sinh (3 * x)))) + (sinh x)) / (((sinh ((5 + 2) * x)) + (2 * (sinh (5 * x)))) + (sinh (3 * x)))
.= (((((sinh (3 * x)) * (cosh (2 * x))) + ((cosh (3 * x)) * (sinh (2 * x)))) + (2 * (sinh (3 * x)))) + (sinh x)) / (((sinh ((5 + 2) * x)) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) by Lm10
.= (((sinh (3 * x)) * ((cosh (2 * x)) + 2)) + (((cosh ((2 * x) + (1 * x))) * (sinh (2 * x))) + (sinh x))) / (((sinh ((5 * x) + (2 * x))) + (2 * (sinh (5 * x)))) + (sinh (3 * x)))
.= (((sinh (3 * x)) * ((cosh (2 * x)) + 2)) + (((((cosh (2 * x)) * (cosh x)) + ((sinh (2 * x)) * (sinh x))) * (sinh (2 * x))) + (sinh x))) / (((sinh ((5 * x) + (2 * x))) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) by Lm10
.= (((sinh (3 * x)) * ((cosh (2 * x)) + 2)) + ((((cosh (2 * x)) * (cosh x)) * (sinh (2 * x))) + ((((sinh (2 * x)) ^2) + 1) * (sinh x)))) / (((sinh ((5 * x) + (2 * x))) + (2 * (sinh (5 * x)))) + (sinh (3 * x)))
.= (((sinh (3 * x)) * ((cosh (2 * x)) + 2)) + ((((cosh (2 * x)) * (cosh x)) * (sinh (2 * x))) + (((((cosh (2 * x)) ^2) - ((sinh (2 * x)) ^2)) + ((sinh (2 * x)) ^2)) * (sinh x)))) / (((sinh ((5 * x) + (2 * x))) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) by Lm3
.= (((sinh (3 * x)) * ((cosh (2 * x)) + 2)) + ((cosh (2 * x)) * (((sinh (2 * x)) * (cosh x)) + ((cosh (2 * x)) * (sinh x))))) / (((sinh ((5 * x) + (2 * x))) + (2 * (sinh (5 * x)))) + (sinh (3 * x)))
.= (((sinh (3 * x)) * ((cosh (2 * x)) + 2)) + ((cosh (2 * x)) * (sinh ((2 * x) + (1 * x))))) / (((sinh ((5 * x) + (2 * x))) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) by Lm10
.= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((((sinh (5 * x)) * (cosh (2 * x))) + ((cosh (5 * x)) * (sinh (2 * x)))) + ((sinh (5 * x)) * 2)) + (sinh (3 * x))) by Lm10
.= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((sinh (5 * x)) * ((cosh (2 * x)) + 2)) + (((cosh ((3 * x) + (2 * x))) * (sinh (2 * x))) + (sinh (3 * x))))
.= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((sinh (5 * x)) * ((cosh (2 * x)) + 2)) + (((((cosh (3 * x)) * (cosh (2 * x))) + ((sinh (3 * x)) * (sinh (2 * x)))) * (sinh (2 * x))) + (sinh (3 * x)))) by Lm10
.= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((sinh (5 * x)) * ((cosh (2 * x)) + 2)) + ((((cosh (3 * x)) * (cosh (2 * x))) * (sinh (2 * x))) + ((sinh (3 * x)) * (((sinh (2 * x)) ^2) + 1))))
.= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((sinh (5 * x)) * ((cosh (2 * x)) + 2)) + ((((cosh (3 * x)) * (cosh (2 * x))) * (sinh (2 * x))) + ((sinh (3 * x)) * ((((cosh (2 * x)) ^2) - ((sinh (2 * x)) ^2)) + ((sinh (2 * x)) ^2))))) by Lm3
.= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((sinh (5 * x)) * ((cosh (2 * x)) + 2)) + ((cosh (2 * x)) * (((sinh (2 * x)) * (cosh (3 * x))) + ((cosh (2 * x)) * (sinh (3 * x))))))
.= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / (((sinh (5 * x)) * ((cosh (2 * x)) + 2)) + ((cosh (2 * x)) * (sinh ((2 * x) + (3 * x))))) by Lm10
.= ((sinh (3 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x)))) / ((sinh (5 * x)) * (((cosh (2 * x)) + 2) + (cosh (2 * x))))
.= (sinh (3 * x)) / (sinh (5 * x)) by Lm13, XCMPLX_1:91 ;
hence (((sinh (5 * x)) + (2 * (sinh (3 * x)))) + (sinh x)) / (((sinh (7 * x)) + (2 * (sinh (5 * x)))) + (sinh (3 * x))) = (sinh (3 * x)) / (sinh (5 * x)) ; :: thesis: verum