let p, r be real number ; :: thesis: ( (sinh . p) + (sinh . r) = (2 * (sinh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (sinh . p) - (sinh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (cosh . ((p / 2) + (r / 2))) )
A1: (2 * (sinh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) = (2 * (((sinh . (p / 2)) * (cosh . (r / 2))) + ((cosh . (p / 2)) * (sinh . (r / 2))))) * (cosh . ((p / 2) - (r / 2))) by Lm4
.= (2 * (((sinh . (p / 2)) * (cosh . (r / 2))) + ((cosh . (p / 2)) * (sinh . (r / 2))))) * (((cosh . (p / 2)) * (cosh . (r / 2))) - ((sinh . (p / 2)) * (sinh . (r / 2)))) by Lm8
.= 2 * (((((sinh . (r / 2)) * (cosh . (r / 2))) * (((cosh . (p / 2)) ^2 ) - ((sinh . (p / 2)) ^2 ))) + ((sinh . (p / 2)) * ((cosh . (p / 2)) * ((cosh . (r / 2)) ^2 )))) - ((cosh . (p / 2)) * ((sinh . (p / 2)) * ((sinh . (r / 2)) ^2 ))))
.= 2 * (((((sinh . (r / 2)) * (cosh . (r / 2))) * 1) + ((sinh . (p / 2)) * ((cosh . (p / 2)) * ((cosh . (r / 2)) ^2 )))) - ((cosh . (p / 2)) * ((sinh . (p / 2)) * ((sinh . (r / 2)) ^2 )))) by Th14
.= 2 * ((((sinh . (p / 2)) * (cosh . (p / 2))) * (((cosh . (r / 2)) ^2 ) - ((sinh . (r / 2)) ^2 ))) + ((sinh . (r / 2)) * (cosh . (r / 2))))
.= 2 * ((((sinh . (p / 2)) * (cosh . (p / 2))) * 1) + ((sinh . (r / 2)) * (cosh . (r / 2)))) by Th14
.= ((2 * (sinh . (p / 2))) * (cosh . (p / 2))) + (2 * ((sinh . (r / 2)) * (cosh . (r / 2))))
.= (sinh . (2 * (p / 2))) + ((2 * (sinh . (r / 2))) * (cosh . (r / 2))) by Lm7
.= (sinh . p) + (sinh . (2 * (r / 2))) by Lm7
.= (sinh . p) + (sinh . r) ;
(2 * (sinh . ((p / 2) - (r / 2)))) * (cosh . ((p / 2) + (r / 2))) = (2 * (((sinh . (p / 2)) * (cosh . (r / 2))) - ((cosh . (p / 2)) * (sinh . (r / 2))))) * (cosh . ((p / 2) + (r / 2))) by Lm9
.= (2 * (((sinh . (p / 2)) * (cosh . (r / 2))) - ((cosh . (p / 2)) * (sinh . (r / 2))))) * (((cosh . (p / 2)) * (cosh . (r / 2))) + ((sinh . (p / 2)) * (sinh . (r / 2)))) by Lm3
.= 2 * (((((cosh . (r / 2)) * (sinh . (r / 2))) * (- (((cosh . (p / 2)) ^2 ) - ((sinh . (p / 2)) ^2 )))) + ((sinh . (p / 2)) * ((cosh . (p / 2)) * ((cosh . (r / 2)) ^2 )))) - ((cosh . (p / 2)) * ((sinh . (p / 2)) * ((sinh . (r / 2)) ^2 ))))
.= 2 * (((((cosh . (r / 2)) * (sinh . (r / 2))) * (- 1)) + ((sinh . (p / 2)) * ((cosh . (p / 2)) * ((cosh . (r / 2)) ^2 )))) - ((cosh . (p / 2)) * ((sinh . (p / 2)) * ((sinh . (r / 2)) ^2 )))) by Th14
.= 2 * ((((sinh . (p / 2)) * (cosh . (p / 2))) * (((cosh . (r / 2)) ^2 ) - ((sinh . (r / 2)) ^2 ))) + ((- 1) * ((cosh . (r / 2)) * (sinh . (r / 2)))))
.= 2 * ((((sinh . (p / 2)) * (cosh . (p / 2))) * 1) + ((- 1) * ((cosh . (r / 2)) * (sinh . (r / 2))))) by Th14
.= ((2 * (sinh . (p / 2))) * (cosh . (p / 2))) - (2 * ((sinh . (r / 2)) * (cosh . (r / 2))))
.= (sinh . (2 * (p / 2))) - ((2 * (sinh . (r / 2))) * (cosh . (r / 2))) by Lm7
.= (sinh . p) - (sinh . (2 * (r / 2))) by Lm7
.= (sinh . p) - (sinh . r) ;
hence ( (sinh . p) + (sinh . r) = (2 * (sinh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (sinh . p) - (sinh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (cosh . ((p / 2) + (r / 2))) ) by A1; :: thesis: verum