let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies sin (arccos r) = sqrt (1 - (r ^2)) )
set s = sqrt (1 - (r ^2));
assume ( - 1 <= r & r <= 1 ) ; :: thesis: sin (arccos r) = sqrt (1 - (r ^2))
then (r ^2) + 0 <= 1 ^2 by SQUARE_1:49;
then 0 <= 1 - (r ^2) by XREAL_1:19;
then ( 0 <= sqrt (1 - (r ^2)) & (r ^2) + ((sqrt (1 - (r ^2))) ^2) = (r ^2) + (1 - (r ^2)) ) by SQUARE_1:def 2;
hence sin (arccos r) = sqrt (1 - (r ^2)) by Th102; :: thesis: verum