theorem :: SIN_COS5:38

for x being Real holds ((sech x) ^2) + ((tanh x) ^2) = 1