let r be Real; :: thesis: ( arcsin is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arcsin,r) = 1 / (sqrt (1 - (r ^2))) ) )
set g = arcsin | ].(- 1),1.[;
set h = sin | [.(- (PI / 2)),(PI / 2).];
set f = sin | ].(- (PI / 2)),(PI / 2).[;
A1: dom (sin | ].(- (PI / 2)),(PI / 2).[) = ].(- (PI / 2)),(PI / 2).[ /\ REAL by RELAT_1:61, SIN_COS:24
.= ].(- (PI / 2)),(PI / 2).[ by XBOOLE_1:28 ;
set x = arcsin . r;
set s = sqrt (1 - (r ^2));
A2: ].(- 1),1.[ c= dom arcsin by Th63, XXREAL_1:25;
A3: sin is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by FDIFF_1:26, SIN_COS:68;
then A4: sin | ].(- (PI / 2)),(PI / 2).[ is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by FDIFF_2:16;

A5: now :: thesis: for x0 being Real st x0 in ].(- (PI / 2)),(PI / 2).[ holds
0 < diff ((sin | ].(- (PI / 2)),(PI / 2).[),x0)

let x0 be Real; :: thesis: ( x0 in ].(- (PI / 2)),(PI / 2).[ implies 0 < diff ((sin | ].(- (PI / 2)),(PI / 2).[),x0) )
assume A6: 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 A4, A6, FDIFF_1:def 7
.= (sin `| ].(- (PI / 2)),(PI / 2).[) . x0 by A3, FDIFF_2:16
.= diff (sin,x0) by A3, A6, FDIFF_1:def 7
.= cos . x0 by SIN_COS:68 ;
hence 0 < diff ((sin | ].(- (PI / 2)),(PI / 2).[),x0) by A6, COMPTRIG:11; :: thesis: verum

end;

A7: (sin | ].(- (PI / 2)),(PI / 2).[) " = ((sin | [.(- (PI / 2)),(PI / 2).]) | ].(- (PI / 2)),(PI / 2).[) " by RELAT_1:74, XXREAL_1:25
.= ((sin | [.(- (PI / 2)),(PI / 2).]) ") | ((sin | [.(- (PI / 2)),(PI / 2).]) .: ].(- (PI / 2)),(PI / 2).[) by RFUNCT_2:17
.= arcsin | ].(- 1),1.[ by Th46, RELAT_1:129, XXREAL_1:25 ;
then A8: ( (sin | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ = sin | ].(- (PI / 2)),(PI / 2).[ & dom ((sin | ].(- (PI / 2)),(PI / 2).[) ") = ].(- 1),1.[ ) by Th63, RELAT_1:62, RELAT_1:72, XXREAL_1:25;
then A9: arcsin | ].(- 1),1.[ is_differentiable_on ].(- 1),1.[ by A7, A4, A1, A5, FDIFF_2:48;
then for x being Real st x in ].(- 1),1.[ holds
arcsin | ].(- 1),1.[ is_differentiable_in x by FDIFF_1:9;
hence A10: arcsin is_differentiable_on ].(- 1),1.[ by A2, FDIFF_1:def 6; :: thesis: ( - 1 < r & r < 1 implies diff (arcsin,r) = 1 / (sqrt (1 - (r ^2))) )
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:49;
arcsin . r = arcsin r ;
then ( - (PI / 2) < arcsin . r & arcsin . r < PI / 2 ) by A11, Th77;
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 A4, FDIFF_1:def 7
.= (sin `| ].(- (PI / 2)),(PI / 2).[) . (arcsin . r) by A3, FDIFF_2:16
.= diff (sin,(arcsin . r)) by A3, A14, FDIFF_1:def 7
.= cos . (arcsin . r) by SIN_COS:68
.= cos (arcsin r) by SIN_COS:def 19
.= sqrt (1 - (r ^2)) by A11, Th81 ;
thus diff (arcsin,r) = (arcsin `| ].(- 1),1.[) . r by A10, A12, FDIFF_1:def 7
.= ((arcsin | ].(- 1),1.[) `| ].(- 1),1.[) . r by A10, FDIFF_2:16
.= diff ((arcsin | ].(- 1),1.[),r) by A9, A12, FDIFF_1:def 7
.= 1 / (sqrt (1 - (r ^2))) by A7, A8, A4, A1, A5, A12, A13, A15, FDIFF_2:48 ; :: thesis: verum