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