theorem Th72: :: SINCOS10:72

for r being Real st 0 < r & r <= PI / 2 holds
arccosec2 (cosec . r) = r