let r be Real; :: 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:61, SIN_COS:24
.= ].0,PI.[ by XBOOLE_1:28 ;
set x = arccos . r;
set s = sqrt (1 - (r ^2));
A2: ].(- 1),1.[ c= dom arccos by Th86, XXREAL_1:25;
A3: cos is_differentiable_on ].0,PI.[ by FDIFF_1:26, SIN_COS:67;
then A4: cos | ].0,PI.[ is_differentiable_on ].0,PI.[ by FDIFF_2:16;

A5: now :: thesis: for x0 being Real st x0 in ].0,PI.[ holds
0 > diff ((cos | ].0,PI.[),x0)

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:7;
diff ((cos | ].0,PI.[),x0) = ((cos | ].0,PI.[) `| ].0,PI.[) . x0 by A4, A6, FDIFF_1:def 7
.= (cos `| ].0,PI.[) . x0 by A3, FDIFF_2:16
.= diff (cos,x0) by A3, A6, FDIFF_1:def 7
.= - (sin . x0) by SIN_COS:67 ;
hence 0 > diff ((cos | ].0,PI.[),x0) by A7; :: thesis: verum

end;

A8: (cos | ].0,PI.[) " = ((cos | [.0,PI.]) | ].0,PI.[) " by RELAT_1:74, XXREAL_1:25
.= ((cos | [.0,PI.]) ") | ((cos | [.0,PI.]) .: ].0,PI.[) by RFUNCT_2:17
.= arccos | ].(- 1),1.[ by Th50, RELAT_1:129, XXREAL_1:25 ;
then A9: ( (cos | ].0,PI.[) | ].0,PI.[ = cos | ].0,PI.[ & dom ((cos | ].0,PI.[) ") = ].(- 1),1.[ ) by Th86, RELAT_1:62, RELAT_1:72, 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:9;
hence A11: arccos is_differentiable_on ].(- 1),1.[ by A2, FDIFF_1:def 6; :: 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:49;
arccos . r = arccos r ;
then ( 0 < arccos . r & arccos . r < PI ) by A12, Th100;
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 7
.= (cos `| ].0,PI.[) . (arccos . r) by A3, FDIFF_2:16
.= diff (cos,(arccos . r)) by A3, A15, FDIFF_1:def 7
.= - (sin . (arccos . r)) by SIN_COS:67
.= - (sin (arccos r)) by SIN_COS:def 17
.= - (sqrt (1 - (r ^2))) by A12, Th104 ;
thus diff (arccos,r) = (arccos `| ].(- 1),1.[) . r by A11, A13, FDIFF_1:def 7
.= ((arccos | ].(- 1),1.[) `| ].(- 1),1.[) . r by A11, FDIFF_2:16
.= diff ((arccos | ].(- 1),1.[),r) by A10, A13, FDIFF_1:def 7
.= 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:192
.= - (1 / (sqrt (1 - (r ^2)))) by XCMPLX_1:187 ; :: thesis: verum