let p be Real; :: thesis: ( (sinh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) - 1) & (cosh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) + 1) )
A1: (cosh . p) ^2 = (((exp_R . p) + (exp_R . (- p))) / 2) * (cosh . p) by Def3
.= (((exp_R . p) + (exp_R . (- p))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2) by Def3
.= (((((exp_R . p) * (exp_R . p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4
.= ((((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) + ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) + (exp_R . (p + (- p)))) + (exp_R . (p + (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= (((exp_R . (2 * p)) + (2 * (exp_R . 0))) + (exp_R . ((- p) + (- p)))) / 4
.= (((exp_R . (2 * p)) + (2 * 1)) + (exp_R . (- (2 * p)))) / 4 by SIN_COS:51, SIN_COS:def 23
.= ((1 / 2) * (((exp_R . (2 * p)) + (exp_R . (- (2 * p)))) / 2)) + ((1 * 2) / (2 * 2))
.= ((1 / 2) * (cosh . (2 * p))) + ((1 / 2) * ((2 * 1) / 2)) by Def3
.= (1 / 2) * ((cosh . (2 * p)) + 1) ;
(sinh . p) ^2 = (((exp_R . p) - (exp_R . (- p))) / 2) * (sinh . p) by Def1
.= (((exp_R . p) - (exp_R . (- p))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2) by Def1
.= (((((exp_R . p) * (exp_R . p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4
.= ((((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + ((exp_R . (- p)) * (exp_R . (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) - ((exp_R . p) * (exp_R . (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) - (exp_R . (p + (- p)))) - ((exp_R . p) * (exp_R . (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= ((((exp_R . (p + p)) + (- (exp_R . (p + (- p))))) - (exp_R . (p + (- p)))) + (exp_R . ((- p) + (- p)))) / 4 by Th12
.= (((exp_R . (2 * p)) + (2 * (- (exp_R . 0)))) + (exp_R . ((- p) + (- p)))) / 4
.= (((exp_R . (2 * p)) + (2 * (- 1))) + (exp_R . (- (2 * p)))) / 4 by SIN_COS:51, SIN_COS:def 23
.= ((1 / 2) * (((exp_R . (2 * p)) + (exp_R . (- (2 * p)))) / 2)) + (((- 1) * 2) / (2 * 2))
.= ((1 / 2) * (cosh . (2 * p))) + ((1 / 2) * ((2 * (- 1)) / 2)) by Def3
.= (1 / 2) * ((cosh . (2 * p)) - 1) ;
hence ( (sinh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) - 1) & (cosh . p) ^2 = (1 / 2) * ((cosh . (2 * p)) + 1) ) by A1; :: thesis: verum