set f = cot | ].0 ,PI .[;
set g = arccot ;
A1: (cot | ].0 ,PI .[) | ].0 ,PI .[ = cot | ].0 ,PI .[ by RELAT_1:101;
A3: 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 X: ].0 ,PI .[ c= dom (cot | ].0 ,PI .[) by Th2, XBOOLE_1:19;
A5: cot | ].0 ,PI .[ is_differentiable_on ].0 ,PI .[ by Lm2, FDIFF_2:16;

now

let x0 be Real; :: thesis: ( x0 in ].0 ,PI .[ implies diff (cot | ].0 ,PI .[),x0 < 0 )
assume A7: x0 in ].0 ,PI .[ ; :: thesis: diff (cot | ].0 ,PI .[),x0 < 0
A8: diff (cot | ].0 ,PI .[),x0 = ((cot | ].0 ,PI .[) `| ].0 ,PI .[) . x0 by A5, A7, FDIFF_1:def 8
.= (cot `| ].0 ,PI .[) . x0 by Lm2, FDIFF_2:16
.= diff cot ,x0 by A7, Lm2, FDIFF_1:def 8
.= - (1 / ((sin . x0) ^2 )) by A7, Lm4 ;
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 A9: (sin . x0) ^2 > 0 by SQUARE_1:74;
1 / ((sin . x0) ^2 ) > 0 / ((sin . x0) ^2 ) by A9, XREAL_1:76;
then - (1 / ((sin . x0) ^2 )) < - 0 by XREAL_1:26;
hence - (1 / ((sin . x0) ^2 )) < 0 ; :: thesis: verum

end;

hence diff (cot | ].0 ,PI .[),x0 < 0 by A7, A8; :: thesis: verum

end;

hence arccot is_differentiable_on cot .: ].0 ,PI .[ by A1, A3, A5, X, FDIFF_2:48; :: thesis: verum