theorem Th102: :: SIN_COS6:102

for r, s being Real st 0 <= s & (r ^2) + (s ^2) = 1 holds
sin (arccos r) = s