let p be Real; :: thesis: ( ((cosh . p) ^2) - ((sinh . p) ^2) = 1 & ((cosh . p) * (cosh . p)) - ((sinh . p) * (sinh . p)) = 1 )
A1: (sinh . p) * (sinh . p) = (((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)))) / (2 * 2)
.= ((((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 + (- p)))) - ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- 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)) - 1) - 1) + (exp_R . ((- p) + (- p)))) / 4 by Th12, Th13 ;
(cosh . p) * (cosh . p) = (((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)))) / (2 * 2)
.= ((((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 + (- p)))) + ((exp_R . (- p)) * (exp_R . p))) + ((exp_R . (- p)) * (exp_R . (- 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)) + 1) + 1) + (exp_R . ((- p) + (- p)))) / 4 by Th12, Th13
.= (((exp_R . (p + p)) + 2) + (exp_R . ((- p) + (- p)))) / 4 ;
hence ( ((cosh . p) ^2) - ((sinh . p) ^2) = 1 & ((cosh . p) * (cosh . p)) - ((sinh . p) * (sinh . p)) = 1 ) by A1; :: thesis: verum