let r be real number ; :: thesis: ( arcsin is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff arcsin ,r = 1 / (sqrt (1 - (r ^2 ))) ) )
set f = sin | ].(- (PI / 2)),(PI / 2).[;
set h = sin | [.(- (PI / 2)),(PI / 2).];
set g = arcsin | ].(- 1),1.[;
A1: (sin | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ = sin | ].(- (PI / 2)),(PI / 2).[ by RELAT_1:101;
A2: (sin | ].(- (PI / 2)),(PI / 2).[) " = ((sin | [.(- (PI / 2)),(PI / 2).]) | ].(- (PI / 2)),(PI / 2).[) " by Lm16, RELAT_1:103
.= ((sin | [.(- (PI / 2)),(PI / 2).]) " ) | ((sin | [.(- (PI / 2)),(PI / 2).]) .: ].(- (PI / 2)),(PI / 2).[) by RFUNCT_2:40
.= arcsin | ].(- 1),1.[ by Lm16, Th46, RELAT_1:162 ;
then A3: dom ((sin | ].(- (PI / 2)),(PI / 2).[) " ) = ].(- 1),1.[ by Lm14, Th64, RELAT_1:91;
A4: sin is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by FDIFF_1:34, SIN_COS:73;
then A5: sin | ].(- (PI / 2)),(PI / 2).[ is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by FDIFF_2:16;
X: dom (sin | ].(- (PI / 2)),(PI / 2).[) = ].(- (PI / 2)),(PI / 2).[ /\ REAL by RELAT_1:90, SIN_COS:27
.= ].(- (PI / 2)),(PI / 2).[ by XBOOLE_1:28 ;

A6: now

let x0 be Real; :: thesis: ( x0 in ].(- (PI / 2)),(PI / 2).[ implies 0 < diff (sin | ].(- (PI / 2)),(PI / 2).[),x0 )
assume A7: x0 in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: 0 < diff (sin | ].(- (PI / 2)),(PI / 2).[),x0
diff (sin | ].(- (PI / 2)),(PI / 2).[),x0 = ((sin | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[) . x0 by A5, A7, FDIFF_1:def 8
.= (sin `| ].(- (PI / 2)),(PI / 2).[) . x0 by A4, FDIFF_2:16
.= diff sin ,x0 by A4, A7, FDIFF_1:def 8
.= cos . x0 by SIN_COS:73 ;
hence 0 < diff (sin | ].(- (PI / 2)),(PI / 2).[),x0 by A7, COMPTRIG:27; :: thesis: verum

end;

then A8: arcsin | ].(- 1),1.[ is_differentiable_on ].(- 1),1.[ by A1, A2, A3, A5, X, FDIFF_2:48;
A9: ].(- 1),1.[ c= dom arcsin by Th64, XXREAL_1:25;
for x being Real st x in ].(- 1),1.[ holds
arcsin | ].(- 1),1.[ is_differentiable_in x by A8, FDIFF_1:16;
hence A10: arcsin is_differentiable_on ].(- 1),1.[ by A9, FDIFF_1:def 7; :: thesis: ( - 1 < r & r < 1 implies diff arcsin ,r = 1 / (sqrt (1 - (r ^2 ))) )
set s = sqrt (1 - (r ^2 ));
set x = arcsin . r;
assume A11: ( - 1 < r & r < 1 ) ; :: thesis: diff arcsin ,r = 1 / (sqrt (1 - (r ^2 )))
then A12: r in ].(- 1),1.[ by XXREAL_1:4;
then A13: (arcsin | ].(- 1),1.[) . r = arcsin . r by FUNCT_1:72;
arcsin . r = arcsin r ;
then ( - (PI / 2) < arcsin . r & arcsin . r < PI / 2 ) by A11, Th78;
then A14: arcsin . r in ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:4;
then A15: diff (sin | ].(- (PI / 2)),(PI / 2).[),(arcsin . r) = ((sin | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[) . (arcsin . r) by A5, FDIFF_1:def 8
.= (sin `| ].(- (PI / 2)),(PI / 2).[) . (arcsin . r) by A4, FDIFF_2:16
.= diff sin ,(arcsin . r) by A4, A14, FDIFF_1:def 8
.= cos . (arcsin . r) by SIN_COS:73
.= cos (arcsin r) by SIN_COS:def 23
.= sqrt (1 - (r ^2 )) by A11, Th82 ;
thus diff arcsin ,r = (arcsin `| ].(- 1),1.[) . r by A10, A12, FDIFF_1:def 8
.= ((arcsin | ].(- 1),1.[) `| ].(- 1),1.[) . r by A10, FDIFF_2:16
.= diff (arcsin | ].(- 1),1.[),r by A8, A12, FDIFF_1:def 8
.= 1 / (sqrt (1 - (r ^2 ))) by A1, A2, A3, A5, A6, A12, A13, A15, X, FDIFF_2:48 ; :: thesis: verum