let A be closed-interval Subset of REAL ; :: thesis: cosh | A is continuous
cosh | REAL is continuous by FDIFF_1:33, SIN_COS2:35;
hence cosh | A is continuous by FCONT_1:17; :: thesis: verum