let p, r be Real; ( (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 Lm8
.=
(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 Lm2
.=
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 Lm6
.=
(sinh . p) - (sinh . (2 * (r / 2)))
by Lm6
.=
(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 Lm3
.=
(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 Lm7
.=
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 Lm6
.=
(sinh . p) + (sinh . (2 * (r / 2)))
by Lm6
.=
(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; verum