set f = cosec | ].0 ,(PI / 2).];
set g = (cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[;
set g1 = arccosec2 | (cosec .: ].0 ,(PI / 2).[);
set X = cosec .: ].0 ,(PI / 2).[;
A0: ].0 ,(PI / 2).[ c= ].0 ,(PI / 2).] by XXREAL_1:21;
then A1: (cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[ = cosec | ].0 ,(PI / 2).[ by RELAT_1:103;
A2: dom ((((cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[) | ].0 ,(PI / 2).[) " ) = rng (((cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[) | ].0 ,(PI / 2).[) by FUNCT_1:55
.= rng (cosec | ].0 ,(PI / 2).[) by A1, RELAT_1:101
.= cosec .: ].0 ,(PI / 2).[ by RELAT_1:148 ;
A3: (cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[ is_differentiable_on ].0 ,(PI / 2).[ by A1, Th8, FDIFF_2:16;

AA: now

let x0 be Real; :: thesis: ( x0 in ].0 ,(PI / 2).[ implies diff ((cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[),x0 < 0 )
assume A4: x0 in ].0 ,(PI / 2).[ ; :: thesis: diff ((cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[),x0 < 0
A5: diff ((cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[),x0 = (((cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[) `| ].0 ,(PI / 2).[) . x0 by A3, A4, FDIFF_1:def 8
.= ((cosec | ].0 ,(PI / 2).[) `| ].0 ,(PI / 2).[) . x0 by A0, RELAT_1:103
.= (cosec `| ].0 ,(PI / 2).[) . x0 by Th8, FDIFF_2:16
.= diff cosec ,x0 by A4, Th8, FDIFF_1:def 8
.= - ((cos . x0) / ((sin . x0) ^2 )) by A4, Th8 ;
for x0 being Real st x0 in ].0 ,(PI / 2).[ holds
- ((cos . x0) / ((sin . x0) ^2 )) < 0

proof

let x0 be Real; :: thesis: ( x0 in ].0 ,(PI / 2).[ implies - ((cos . x0) / ((sin . x0) ^2 )) < 0 )
assume A6: x0 in ].0 ,(PI / 2).[ ; :: thesis: - ((cos . x0) / ((sin . x0) ^2 )) < 0
].0 ,(PI / 2).[ c= ].0 ,PI .[ by COMPTRIG:21, XXREAL_1:46;
then sin . x0 > 0 by A6, COMPTRIG:23;
then A7: (sin . x0) ^2 > 0 ;
].0 ,(PI / 2).[ 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 | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[),x0 < 0 by A4, A5; :: thesis: verum

end;

AB: (((cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[) | ].0 ,(PI / 2).[) " = ((cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[) " by RELAT_1:101
.= arccosec2 | ((cosec | ].0 ,(PI / 2).]) .: ].0 ,(PI / 2).[) by RFUNCT_2:40
.= arccosec2 | (rng ((cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[)) by RELAT_1:148
.= arccosec2 | (rng (cosec | ].0 ,(PI / 2).[)) by A0, RELAT_1:103
.= arccosec2 | (cosec .: ].0 ,(PI / 2).[) by RELAT_1:148 ;
then A9: arccosec2 | (cosec .: ].0 ,(PI / 2).[) is_differentiable_on cosec .: ].0 ,(PI / 2).[ by A2, A3, AA, X18, FDIFF_2:48;
A11: cosec .: ].0 ,(PI / 2).[ c= dom arccosec2 by A2, AB, RELAT_1:89;
for x being Real st x in cosec .: ].0 ,(PI / 2).[ holds
arccosec2 | (cosec .: ].0 ,(PI / 2).[) is_differentiable_in x

proof

let x be Real; :: thesis: ( x in cosec .: ].0 ,(PI / 2).[ implies arccosec2 | (cosec .: ].0 ,(PI / 2).[) is_differentiable_in x )
assume x in cosec .: ].0 ,(PI / 2).[ ; :: thesis: arccosec2 | (cosec .: ].0 ,(PI / 2).[) is_differentiable_in x
then (arccosec2 | (cosec .: ].0 ,(PI / 2).[)) | (cosec .: ].0 ,(PI / 2).[) is_differentiable_in x by A9, FDIFF_1:def 7;
hence arccosec2 | (cosec .: ].0 ,(PI / 2).[) is_differentiable_in x by RELAT_1:101; :: thesis: verum

end;

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