set f = cosec | [.(- (PI / 2)),0 .[;
set g = (cosec | [.(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[;
set g1 = arccosec1 | (cosec .: ].(- (PI / 2)),0 .[);
set X = cosec .: ].(- (PI / 2)),0 .[;
A0: ].(- (PI / 2)),0 .[ c= [.(- (PI / 2)),0 .[ by XXREAL_1:22;
then A1: (cosec | [.(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[ = cosec | ].(- (PI / 2)),0 .[ by RELAT_1:103;
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:55
.= rng (cosec | ].(- (PI / 2)),0 .[) by A1, RELAT_1:101
.= cosec .: ].(- (PI / 2)),0 .[ by RELAT_1:148 ;
A3: (cosec | [.(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[ is_differentiable_on ].(- (PI / 2)),0 .[ by A1, Th7, FDIFF_2:16;

AA: now

let x0 be Real; :: thesis: ( x0 in ].(- (PI / 2)),0 .[ implies diff ((cosec | [.(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[),x0 < 0 )
assume A4: x0 in ].(- (PI / 2)),0 .[ ; :: thesis: diff ((cosec | [.(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[),x0 < 0
A5: diff ((cosec | [.(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[),x0 = (((cosec | [.(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[) `| ].(- (PI / 2)),0 .[) . x0 by A3, A4, FDIFF_1:def 8
.= ((cosec | ].(- (PI / 2)),0 .[) `| ].(- (PI / 2)),0 .[) . x0 by A0, RELAT_1:103
.= (cosec `| ].(- (PI / 2)),0 .[) . x0 by Th7, FDIFF_2:16
.= diff cosec ,x0 by A4, Th7, FDIFF_1:def 8
.= - ((cos . x0) / ((sin . x0) ^2 )) by A4, Th7 ;
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
].(- (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, XBOOLE_1:1;
then ( - PI < x0 & x0 < 0 ) by A6, XXREAL_1:4;
then ( (- PI ) + (2 * PI ) < x0 + (2 * PI ) & x0 + (2 * PI ) < 0 + (2 * PI ) ) by XREAL_1:10;
then x0 + (2 * PI ) in ].PI ,(2 * PI ).[ ;
then sin . (x0 + (2 * PI )) < 0 by COMPTRIG:25;
then sin . x0 < 0 by SIN_COS:83;
then A7: (sin . x0) ^2 > 0 ;
].(- (PI / 2)),0 .[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46;
then cos . x0 > 0 by A6, COMPTRIG:27;
then (cos . x0) / ((sin . x0) ^2 ) > 0 / ((sin . x0) ^2 ) by A7;
then - ((cos . x0) / ((sin . x0) ^2 )) < - 0 ;
hence - ((cos . x0) / ((sin . x0) ^2 )) < 0 ; :: thesis: verum

end;

hence diff ((cosec | [.(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[),x0 < 0 by A4, A5; :: thesis: verum

end;

AB: (((cosec | [.(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[) " = ((cosec | [.(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[) " by RELAT_1:101
.= arccosec1 | ((cosec | [.(- (PI / 2)),0 .[) .: ].(- (PI / 2)),0 .[) by RFUNCT_2:40
.= arccosec1 | (rng ((cosec | [.(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[)) by RELAT_1:148
.= arccosec1 | (rng (cosec | ].(- (PI / 2)),0 .[)) by A0, RELAT_1:103
.= arccosec1 | (cosec .: ].(- (PI / 2)),0 .[) by RELAT_1:148 ;
then A9: arccosec1 | (cosec .: ].(- (PI / 2)),0 .[) is_differentiable_on cosec .: ].(- (PI / 2)),0 .[ by A2, A3, AA, X17, FDIFF_2:48;
A11: cosec .: ].(- (PI / 2)),0 .[ c= dom arccosec1 by A2, AB, RELAT_1:89;
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 A9, FDIFF_1:def 7;
hence arccosec1 | (cosec .: ].(- (PI / 2)),0 .[) is_differentiable_in x by RELAT_1:101; :: thesis: verum

end;

hence arccosec1 is_differentiable_on cosec .: ].(- (PI / 2)),0 .[ by A11, FDIFF_1:def 7; :: thesis: verum