set g = arccot ;
set f = cot | ].0 ,PI .[;
A1: dom ((cot | ].0 ,PI .[) " ) = rng (cot | ].0 ,PI .[) by FUNCT_1:55
.= cot .: ].0 ,PI .[ by RELAT_1:148 ;
dom (cot | ].0 ,PI .[) = (dom cot ) /\ ].0 ,PI .[ by RELAT_1:90;
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

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:23;
then (sin . x0) ^2 > 0 by SQUARE_1:74;
then 1 / ((sin . x0) ^2 ) > 0 / ((sin . x0) ^2 ) by XREAL_1:76;
then - (1 / ((sin . x0) ^2 )) < - 0 by XREAL_1:26;
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 8
.= (cot `| ].0 ,PI .[) . x0 by Lm2, FDIFF_2:16
.= diff cot ,x0 by A6, Lm2, FDIFF_1:def 8
.= - (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:101;
hence arccot is_differentiable_on cot .: ].0 ,PI .[ by A1, A2, A3, A4, FDIFF_2:48; :: thesis: verum