let p be Real; :: thesis: ( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) )
A1: cosh . (- p) = ((exp_R . (- p)) + (exp_R . (- (- p)))) / 2 by Def3
.= cosh . p by Def3 ;
A2: sinh . (- p) = ((exp_R . (- p)) - (exp_R . (- (- p)))) / 2 by Def1
.= - (((exp_R . p) - (exp_R . (- p))) / 2)
.= - (sinh . p) by Def1 ;
then tanh . (- p) = (- (sinh . p)) / (cosh . (- p)) by Th17
.= - ((sinh . p) / (cosh . p)) by A1, XCMPLX_1:187
.= - (tanh . p) by Th17 ;
hence ( cosh . (- p) = cosh . p & sinh . (- p) = - (sinh . p) & tanh . (- p) = - (tanh . p) ) by A1, A2; :: thesis: verum