let p be real number ; :: thesis: ( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 )
A1: cosh . 0 = 1

proof

cosh . 0 = ((exp_R . 0 ) + (exp_R . (- 0 ))) / 2 by Def3
.= 1 by SIN_COS:56, SIN_COS:def 27 ;
hence cosh . 0 = 1 ; :: thesis: verum

end;

cosh . p > 0

proof

( exp_R . p > 0 & exp_R . (- p) > 0 ) by SIN_COS:59;
then (exp_R . p) + (exp_R . (- p)) > 0 + 0 ;
then ((exp_R . p) + (exp_R . (- p))) / 2 > 0 by XREAL_1:141;
hence cosh . p > 0 by Def3; :: thesis: verum

end;

hence ( cosh . p <> 0 & cosh . p > 0 & cosh . 0 = 1 ) by A1; :: thesis: verum