let r be Real; :: 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 Th62, Th63, FUNCT_1:def 3;
thus sin (arcsin r) = sin . (arcsin . r) by SIN_COS:def 17
.= (sin | [.(- (PI / 2)),(PI / 2).]) . (arcsin . r) by A2, FUNCT_1:49
.= (id [.(- 1),1.]) . r by A1, Th63, Th64, FUNCT_1:13
.= r by A1, FUNCT_1:18 ; :: thesis: verum