theorem Th81: :: SIN_COS6:81

for r being Real st - 1 <= r & r <= 1 holds
cos (arcsin r) = sqrt (1 - (r ^2))