let p, r be Real; :: thesis: cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r))
((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) = ((((exp_R . p) + (exp_R . (- p))) / 2) * (cosh . r)) + ((sinh . p) * (sinh . r)) by Def3
.= ((((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . r) + (exp_R . (- r))) / 2)) + ((sinh . 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 Def1
.= ((((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
.= cosh . (p + r) by Def3 ;
hence cosh . (p + r) = ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) ; :: thesis: verum