theorem :: SIN_COS7:47

for x being Real st x > 0 & x <= 1 holds
sech1" x = cosh1" (1 / x)