let p be Real; ( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 )
A1: 2 * ((cosh . p) ^2) =
2 * ((1 / 2) * ((cosh . (2 * p)) + 1))
by Th18
.=
(cosh . (2 * p)) + 1
;
(2 * (sinh . p)) * (cosh . p) =
(2 * (((exp_R . p) - (exp_R . (- p))) / 2)) * (cosh . p)
by Def1
.=
(2 * (((exp_R . p) - (exp_R . (- p))) / 2)) * (((exp_R . p) + (exp_R . (- p))) / 2)
by Def3
.=
(2 / 4) * (((exp_R . p) ^2) - ((exp_R . (- p)) ^2))
.=
(2 / 4) * ((exp_R . (p + p)) - ((exp_R . (- p)) * (exp_R . (- p))))
by Th12
.=
(2 / 4) * ((exp_R . (2 * p)) - (exp_R . ((- p) + (- p))))
by Th12
.=
(((exp_R . (2 * p)) - (exp_R . (- (2 * p)))) / 2) * 1
.=
sinh . (2 * p)
by Def1
;
hence
( sinh . (2 * p) = (2 * (sinh . p)) * (cosh . p) & cosh . (2 * p) = (2 * ((cosh . p) ^2)) - 1 )
by A1; verum