theorem :: SIN_COS2:39
for p being Real holds cosh is_continuous_in p by Th32, FDIFF_1:24;