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