let x be Real; :: thesis: ( tanh x = (sinh x) / (cosh x) & tanh 0 = 0 )

A1: tanh 0 = tanh . 0 by SIN_COS2:def 6

.= (sinh . 0) / (cosh . 0) by SIN_COS2:17

.= 0 by SIN_COS2:16 ;

tanh x = tanh . x by SIN_COS2:def 6

.= (sinh . x) / (cosh . x) by SIN_COS2:17

.= (sinh x) / (cosh . x) by SIN_COS2:def 2

.= (sinh x) / (cosh x) by SIN_COS2:def 4 ;

hence ( tanh x = (sinh x) / (cosh x) & tanh 0 = 0 ) by A1; :: thesis: verum

A1: tanh 0 = tanh . 0 by SIN_COS2:def 6

.= (sinh . 0) / (cosh . 0) by SIN_COS2:17

.= 0 by SIN_COS2:16 ;

tanh x = tanh . x by SIN_COS2:def 6

.= (sinh . x) / (cosh . x) by SIN_COS2:17

.= (sinh x) / (cosh . x) by SIN_COS2:def 2

.= (sinh x) / (cosh x) by SIN_COS2:def 4 ;

hence ( tanh x = (sinh x) / (cosh x) & tanh 0 = 0 ) by A1; :: thesis: verum