theorem :: SIN_COS7:33

for x being Real st 0 <= x holds
sinh" x = cosh1" (sqrt ((x ^2) + 1))