let r be real number ; :: thesis: ( - 1 <= r & r <= 1 implies sin (arcsin r) = r )
assume ( - 1 <= r & r <= 1 ) ; :: thesis: sin (arcsin r) = r
then A1: r in [.(- 1),1.] by XXREAL_1:1;
then A2: arcsin . r in [.(- (PI / 2)),(PI / 2).] by Th63, Th64, FUNCT_1:def 5;
thus sin (arcsin r) = sin . (arcsin . r) by SIN_COS:def 21
.= (sin | [.(- (PI / 2)),(PI / 2).]) . (arcsin . r) by A2, FUNCT_1:72
.= (id [.(- 1),1.]) . r by A1, Th64, Th65, FUNCT_1:23
.= r by A1, FUNCT_1:35 ; :: thesis: verum