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

A6: now

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

end;

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