let x be Real; :: thesis: sinh (3 * x) = (3 * (sinh x)) + (4 * ((sinh x) |^ 3))
sinh (3 * x) = sinh . ((x + x) + x) by SIN_COS2:def 2
.= ((sinh . (2 * x)) * (cosh . x)) + ((cosh . (2 * x)) * (sinh . x)) by SIN_COS2:21
.= (((2 * (sinh . x)) * (cosh . x)) * (cosh . x)) + ((cosh . (2 * x)) * (sinh . x)) by SIN_COS2:23
.= ((2 * (sinh . x)) * ((cosh . x) ^2)) + (((2 * ((cosh . x) ^2)) - 1) * (sinh . x)) by SIN_COS2:23
.= ((2 * (sinh . x)) * (1 + ((sinh . x) ^2))) + (((2 * ((cosh . x) ^2)) - 1) * (sinh . x)) by Lm2
.= ((2 * (sinh . x)) * (1 + ((sinh . x) ^2))) + (((2 * (1 + ((sinh . x) ^2))) - 1) * (sinh . x)) by Lm2
.= ((2 * (sinh . x)) + (((2 + 2) * (sinh . x)) * ((sinh . x) ^2))) + (sinh . x)
.= ((2 * (sinh . x)) + ((4 * ((sinh . x) |^ 1)) * ((sinh . x) ^2))) + (sinh . x)
.= (3 * (sinh . x)) + (4 * ((((sinh . x) |^ 1) * (sinh . x)) * (sinh . x)))
.= (3 * (sinh . x)) + (4 * (((sinh . x) |^ (1 + 1)) * (sinh . x))) by NEWTON:6
.= (3 * (sinh . x)) + (4 * ((sinh . x) |^ (2 + 1))) by NEWTON:6
.= (3 * (sinh x)) + (4 * ((sinh . x) |^ 3)) by SIN_COS2:def 2 ;
hence sinh (3 * x) = (3 * (sinh x)) + (4 * ((sinh x) |^ 3)) by SIN_COS2:def 2; :: thesis: verum