let r be real number ; :: thesis: ( - 1 <= r & r <= 1 implies (arcsin r) + (arccos r) = PI / 2 )
assume A1: ( - 1 <= r & r <= 1 ) ; :: thesis: (arcsin r) + (arccos r) = PI / 2
then ( (- (PI / 2)) + (PI / 2) <= arccos r & arccos r <= (PI / 2) + (PI / 2) ) by Th101;
then ( - (PI / 2) <= (arccos r) - (PI / 2) & (arccos r) - (PI / 2) <= PI / 2 ) by XREAL_1:21, XREAL_1:22;
then A2: ( - (- (PI / 2)) >= - ((arccos r) - (PI / 2)) & - ((arccos r) - (PI / 2)) >= - (PI / 2) ) by XREAL_1:26;
r = ((sin (PI / 2)) * (cos (arccos r))) - ((cos (PI / 2)) * (sin (arccos r))) by A1, Th93, SIN_COS:82
.= sin ((PI / 2) - (arccos r)) by COMPLEX2:4 ;
then arcsin r = (PI / 2) - (arccos r) by A2, Th70;
hence (arcsin r) + (arccos r) = PI / 2 ; :: thesis: verum