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