:: deftheorem defines arccosec2 SINCOS10:def 8 :
for r being Real holds arccosec2 r = arccosec2 . r;