let p, r be Real; :: thesis: sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))
((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) = ((((exp_R . p) - (exp_R . (- p))) / 2) * (cosh . r)) + ((cosh . p) * (sinh . r)) by Def1
.= ((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((cosh . p) * (sinh . r)) by Def3
.= ((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((((exp_R . p) + (exp_R . (- p))) / 2) * (sinh . r)) by Def3
.= ((((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . r) - (exp_R . (- r))) / 2)) by Def1
.= ((2 * ((exp_R . p) * (exp_R . r))) + (2 * (- ((exp_R . (- p)) * (exp_R . (- r)))))) / 4
.= ((2 * (exp_R . (p + r))) + (2 * (- ((exp_R . (- p)) * (exp_R . (- r)))))) / 4 by Th12
.= ((2 * (exp_R . (p + r))) + (2 * (- (exp_R . ((- p) + (- r)))))) / 4 by Th12
.= ((exp_R . (p + r)) - (exp_R . (- (p + r)))) / 2
.= sinh . (p + r) by Def1 ;
hence sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) ; :: thesis: verum