let r be Real; :: thesis: ( - (PI / 2) <= r & r <= PI / 2 implies arcsin (sin r) = r )
A1: dom (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- (PI / 2)),(PI / 2).] by RELAT_1:62, SIN_COS:24;
assume ( - (PI / 2) <= r & r <= PI / 2 ) ; :: thesis: arcsin (sin r) = r
then A2: r in [.(- (PI / 2)),(PI / 2).] by XXREAL_1:1;
thus arcsin (sin r) = arcsin . (sin . r) by SIN_COS:def 17
.= arcsin . ((sin | [.(- (PI / 2)),(PI / 2).]) . r) by A2, FUNCT_1:49
.= (id [.(- (PI / 2)),(PI / 2).]) . r by A2, A1, Th66, FUNCT_1:13
.= r by A2, FUNCT_1:18 ; :: thesis: verum