let r be real number ; :: thesis: ( - 1 <= r & r <= 1 implies cos (arcsin r) = sqrt (1 - (r ^2 )) )
set s = sqrt (1 - (r ^2 ));
assume ( - 1 <= r & r <= 1 ) ; :: thesis: cos (arcsin r) = sqrt (1 - (r ^2 ))
then (r ^2 ) + 0 <= 1 ^2 by SQUARE_1:119;
then 0 <= 1 - (r ^2 ) by XREAL_1:21;
then ( 0 <= sqrt (1 - (r ^2 )) & (r ^2 ) + ((sqrt (1 - (r ^2 ))) ^2 ) = (r ^2 ) + (1 - (r ^2 )) ) by SQUARE_1:def 4;
hence cos (arcsin r) = sqrt (1 - (r ^2 )) by Th80; :: thesis: verum