let p be Real; :: thesis: ( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 )
( exp_R . p > 0 & exp_R . (- p) > 0 ) by SIN_COS:54;
then A1: ((exp_R . p) + (exp_R . (- p))) / 2 > 0 by XREAL_1:139;
cosh . 0 = ((exp_R . 0) + (exp_R . (- 0))) / 2 by Def3
.= 1 by SIN_COS:51, SIN_COS:def 23 ;
hence ( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 ) by A1, Def3; :: thesis: verum