let x be Real; :: thesis: ((cosh x) + (sinh x)) / ((cosh x) - (sinh x)) = (1 + (tanh x)) / (1 - (tanh x))
A1: exp_R (2 * x) = (1 + (tanh x)) / (1 - (tanh ((2 * x) / 2))) by Th7
.= (1 + (tanh x)) / (1 - (tanh x)) ;
exp_R (2 * x) = ((cosh ((2 * x) / 2)) + (sinh ((2 * x) / 2))) / ((cosh ((2 * x) / 2)) - (sinh ((2 * x) / 2))) by Th7
.= ((cosh x) + (sinh x)) / ((cosh x) - (sinh x)) ;
hence ((cosh x) + (sinh x)) / ((cosh x) - (sinh x)) = (1 + (tanh x)) / (1 - (tanh x)) by A1; :: thesis: verum