let p be Real; :: thesis: ( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 & tanh . (2 * p) = (2 * (tanh . p)) / (1 + ((tanh . p) ^2)) )
tanh . (2 * p) = tanh . (p + p)
.= ((tanh . p) + (tanh . p)) / (1 + ((tanh . p) * (tanh . p))) by Lm5
.= (2 * (tanh . p)) / (1 + ((tanh . p) ^2)) ;
hence ( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 & tanh . (2 * p) = (2 * (tanh . p)) / (1 + ((tanh . p) ^2)) ) by Lm6; :: thesis: verum