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