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 g = arccos | ].(- 1),1.[;
set h = cos | [.0 ,PI .];
set f = cos | ].0 ,PI .[;
A1: dom (cos | ].0 ,PI .[) = ].0 ,PI .[ /\ REAL by RELAT_1:90, SIN_COS:27
.= ].0 ,PI .[ by XBOOLE_1:28 ;
set x = arccos . r;
set s = sqrt (1 - (r ^2 ));
A2: ].(- 1),1.[ c= dom arccos by Th88, XXREAL_1:25;
A3: cos is_differentiable_on ].0 ,PI .[ by FDIFF_1:34, SIN_COS:72;
then A4: cos | ].0 ,PI .[ is_differentiable_on ].0 ,PI .[ by FDIFF_2:16;

A5: now

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

end;

A8: (cos | ].0 ,PI .[) " = ((cos | [.0 ,PI .]) | ].0 ,PI .[) " by RELAT_1:103, XXREAL_1:25
.= ((cos | [.0 ,PI .]) " ) | ((cos | [.0 ,PI .]) .: ].0 ,PI .[) by RFUNCT_2:40
.= arccos | ].(- 1),1.[ by Th50, RELAT_1:162, XXREAL_1:25 ;
then A9: ( (cos | ].0 ,PI .[) | ].0 ,PI .[ = cos | ].0 ,PI .[ & dom ((cos | ].0 ,PI .[) " ) = ].(- 1),1.[ ) by Th88, RELAT_1:91, RELAT_1:101, XXREAL_1:25;
then A10: arccos | ].(- 1),1.[ is_differentiable_on ].(- 1),1.[ by A8, A4, A1, A5, FDIFF_2:48;
then for x being Real st x in ].(- 1),1.[ holds
arccos | ].(- 1),1.[ is_differentiable_in x by FDIFF_1:16;
hence A11: arccos is_differentiable_on ].(- 1),1.[ by A2, FDIFF_1:def 7; :: thesis: ( - 1 < r & r < 1 implies diff arccos ,r = - (1 / (sqrt (1 - (r ^2 )))) )
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 A4, FDIFF_1:def 8
.= (cos `| ].0 ,PI .[) . (arccos . r) by A3, FDIFF_2:16
.= diff cos ,(arccos . r) by A3, 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 A10, A13, FDIFF_1:def 8
.= 1 / (- (sqrt (1 - (r ^2 )))) by A8, A9, A4, A1, A5, A13, A14, A16, FDIFF_2:48
.= (- 1) / (sqrt (1 - (r ^2 ))) by XCMPLX_1:193
.= - (1 / (sqrt (1 - (r ^2 )))) by XCMPLX_1:188 ; :: thesis: verum