let r, s be Real; :: thesis: ( 0 <= s & (r ^2) + (s ^2) = 1 implies sin (arccos r) = s )
set x = arccos r;
assume that
A1: 0 <= s and
A2: (r ^2) + (s ^2) = 1 ; :: thesis: sin (arccos r) = s
A3: ( - 1 <= r & r <= 1 ) by A2, Lm5;
then ( 0 <= arccos r & arccos r <= PI ) by Th99;
then A4: arccos r in [.0,PI.] by XXREAL_1:1;
((sin . (arccos r)) ^2) + ((cos . (arccos r)) ^2) = 1 by SIN_COS:28;
then (sin . (arccos r)) ^2 = 1 - ((cos . (arccos r)) ^2)
.= 1 - ((cos (arccos r)) ^2) by SIN_COS:def 19
.= 1 - (r ^2) by A3, Th91 ;
then A5: ( sin . (arccos r) = s or sin . (arccos r) = - s ) by A2, SQUARE_1:40;
( - (- (- s)) < 0 or s = 0 ) by A1;
hence sin (arccos r) = s by A5, A4, COMPTRIG:8, SIN_COS:def 17; :: thesis: verum