theorem :: SIN_COS2:40
for p being Real holds tanh is_continuous_in p by Lm22, Lm23, FDIFF_1:24;