theorem :: SIN_COS7:49

for x being Real st x > 0 holds
csch" x = sinh" (1 / x)