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