let p, r be Real; :: thesis: ( (cosh . p) + (cosh . r) = (2 * (cosh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (cosh . p) - (cosh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (sinh . ((p / 2) + (r / 2))) )
A1: (2 * (sinh . ((p / 2) - (r / 2)))) * (sinh . ((p / 2) + (r / 2))) = 2 * ((sinh . ((p / 2) - (r / 2))) * (sinh . ((p / 2) + (r / 2))))
.= 2 * (((cosh . (p / 2)) ^2) - ((cosh . (r / 2)) ^2)) by Th24
.= 2 * (((1 / 2) * ((cosh . (2 * (p / 2))) + 1)) - ((cosh . (r / 2)) ^2)) by Th18
.= 2 * (((1 / 2) * ((cosh . p) + 1)) - ((1 / 2) * ((cosh . (2 * (r / 2))) + 1))) by Th18
.= (cosh . p) - (cosh . r) ;
(2 * (cosh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) = 2 * ((cosh . ((p / 2) + (r / 2))) * (cosh . ((p / 2) - (r / 2))))
.= 2 * (((sinh . (p / 2)) ^2) + ((cosh . (r / 2)) ^2)) by Th25
.= 2 * (((1 / 2) * ((cosh . (2 * (p / 2))) - 1)) + ((cosh . (r / 2)) ^2)) by Th18
.= 2 * (((1 / 2) * ((cosh . p) - 1)) + ((1 / 2) * ((cosh . (2 * (r / 2))) + 1))) by Th18
.= (cosh . r) + (cosh . p) ;
hence ( (cosh . p) + (cosh . r) = (2 * (cosh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (cosh . p) - (cosh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (sinh . ((p / 2) + (r / 2))) ) by A1; :: thesis: verum