theorem :: SIN_COS6:83

for r being Real holds
( arcsin is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arcsin,r) = 1 / (sqrt (1 - (r ^2))) ) )