set X = cosec .: ].(- (PI / 2)),0.[;
set g1 = arccosec1 | (cosec .: ].(- (PI / 2)),0.[);
set f = cosec | [.(- (PI / 2)),0.[;
set g = (cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[;
A1: (cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[ = cosec | ].(- (PI / 2)),0.[ by RELAT_1:74, XXREAL_1:22;
A2: dom ((((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) ") = rng (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) by FUNCT_1:33
.= rng (cosec | ].(- (PI / 2)),0.[) by A1, RELAT_1:72
.= cosec .: ].(- (PI / 2)),0.[ by RELAT_1:115 ;
A3: (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) " = ((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) " by RELAT_1:72
.= arccosec1 | ((cosec | [.(- (PI / 2)),0.[) .: ].(- (PI / 2)),0.[) by RFUNCT_2:17
.= arccosec1 | (rng ((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[)) by RELAT_1:115
.= arccosec1 | (rng (cosec | ].(- (PI / 2)),0.[)) by RELAT_1:74, XXREAL_1:22
.= arccosec1 | (cosec .: ].(- (PI / 2)),0.[) by RELAT_1:115 ;
A4: (cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[ is_differentiable_on ].(- (PI / 2)),0.[ by A1, Th7, FDIFF_2:16;

now :: thesis: for x0 being Real st x0 in ].(- (PI / 2)),0.[ holds
diff (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[),x0) < 0

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

proof

let x0 be Real; :: thesis: ( x0 in ].(- (PI / 2)),0.[ implies - ((cos . x0) / ((sin . x0) ^2)) < 0 )
assume A6: x0 in ].(- (PI / 2)),0.[ ; :: thesis: - ((cos . x0) / ((sin . x0) ^2)) < 0
then x0 < 0 by XXREAL_1:4;
then A7: x0 + (2 * PI) < 0 + (2 * PI) by XREAL_1:8;
].(- (PI / 2)),0.[ \/ {(- (PI / 2))} = [.(- (PI / 2)),0.[ by XXREAL_1:131;
then ].(- (PI / 2)),0.[ c= [.(- (PI / 2)),0.[ by XBOOLE_1:7;
then ].(- (PI / 2)),0.[ c= ].(- PI),0.[ by Lm3;
then - PI < x0 by A6, XXREAL_1:4;
then (- PI) + (2 * PI) < x0 + (2 * PI) by XREAL_1:8;
then x0 + (2 * PI) in ].PI,(2 * PI).[ by A7;
then sin . (x0 + (2 * PI)) < 0 by COMPTRIG:9;
then A8: sin . x0 < 0 by SIN_COS:78;
].(- (PI / 2)),0.[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46;
then cos . x0 > 0 by A6, COMPTRIG:11;
hence - ((cos . x0) / ((sin . x0) ^2)) < 0 by A8; :: thesis: verum

end;

let x0 be Real; :: thesis: ( x0 in ].(- (PI / 2)),0.[ implies diff (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[),x0) < 0 )
assume A9: x0 in ].(- (PI / 2)),0.[ ; :: thesis: diff (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[),x0) < 0
diff (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[),x0) = (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) `| ].(- (PI / 2)),0.[) . x0 by A4, A9, FDIFF_1:def 7
.= ((cosec | ].(- (PI / 2)),0.[) `| ].(- (PI / 2)),0.[) . x0 by RELAT_1:74, XXREAL_1:22
.= (cosec `| ].(- (PI / 2)),0.[) . x0 by Th7, FDIFF_2:16
.= diff (cosec,x0) by A9, Th7, FDIFF_1:def 7
.= - ((cos . x0) / ((sin . x0) ^2)) by A9, Th7 ;
hence diff (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[),x0) < 0 by A9, A5; :: thesis: verum

end;

then A10: arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is_differentiable_on cosec .: ].(- (PI / 2)),0.[ by A2, A4, A3, Lm23, FDIFF_2:48;
A11: for x being Real st x in cosec .: ].(- (PI / 2)),0.[ holds
arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is_differentiable_in x

proof

let x be Real; :: thesis: ( x in cosec .: ].(- (PI / 2)),0.[ implies arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is_differentiable_in x )
assume x in cosec .: ].(- (PI / 2)),0.[ ; :: thesis: arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is_differentiable_in x
then (arccosec1 | (cosec .: ].(- (PI / 2)),0.[)) | (cosec .: ].(- (PI / 2)),0.[) is_differentiable_in x by A10, FDIFF_1:def 6;
hence arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is_differentiable_in x by RELAT_1:72; :: thesis: verum

end;

cosec .: ].(- (PI / 2)),0.[ c= dom arccosec1 by A2, A3, RELAT_1:60;
hence arccosec1 is_differentiable_on cosec .: ].(- (PI / 2)),0.[ by A11, FDIFF_1:def 6; :: thesis: verum