set f = cot | ].0,PI.[;
A1: dom ((cot | ].0,PI.[) ") = rng (cot | ].0,PI.[) by FUNCT_1:33
.= cot .: ].0,PI.[ by RELAT_1:115 ;
dom (cot | ].0,PI.[) = (dom cot) /\ ].0,PI.[ by RELAT_1:61;
then A2: ].0,PI.[ c= dom (cot | ].0,PI.[) by Th2, XBOOLE_1:19;
A3: cot | ].0,PI.[ is_differentiable_on ].0,PI.[ by Lm2, FDIFF_2:16;

A4: now :: thesis: for x0 being Real st x0 in ].0,PI.[ holds
diff ((cot | ].0,PI.[),x0) < 0

A5: for x0 being Real st x0 in ].0,PI.[ holds
- (1 / ((sin . x0) ^2)) < 0

proof

let x0 be Real; :: thesis: ( x0 in ].0,PI.[ implies - (1 / ((sin . x0) ^2)) < 0 )
assume x0 in ].0,PI.[ ; :: thesis: - (1 / ((sin . x0) ^2)) < 0
then 0 < sin . x0 by COMPTRIG:7;
then (sin . x0) ^2 > 0 ;
then 1 / ((sin . x0) ^2) > 0 / ((sin . x0) ^2) ;
then - (1 / ((sin . x0) ^2)) < - 0 ;
hence - (1 / ((sin . x0) ^2)) < 0 ; :: thesis: verum

end;

let x0 be Real; :: thesis: ( x0 in ].0,PI.[ implies diff ((cot | ].0,PI.[),x0) < 0 )
assume A6: x0 in ].0,PI.[ ; :: thesis: diff ((cot | ].0,PI.[),x0) < 0
diff ((cot | ].0,PI.[),x0) = ((cot | ].0,PI.[) `| ].0,PI.[) . x0 by A3, A6, FDIFF_1:def 7
.= (cot `| ].0,PI.[) . x0 by Lm2, FDIFF_2:16
.= diff (cot,x0) by A6, Lm2, FDIFF_1:def 7
.= - (1 / ((sin . x0) ^2)) by A6, Lm4 ;
hence diff ((cot | ].0,PI.[),x0) < 0 by A6, A5; :: thesis: verum

end;

(cot | ].0,PI.[) | ].0,PI.[ = cot | ].0,PI.[ by RELAT_1:72;
hence arccot is_differentiable_on cot .: ].0,PI.[ by A1, A2, A3, A4, FDIFF_2:48; :: thesis: verum