set X = cosec .: ].0,(PI / 2).[;
set g1 = arccosec2 | (cosec .: ].0,(PI / 2).[);
set f = cosec | ].0,(PI / 2).];
set g = (cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[;
A1:
(cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[ = cosec | ].0,(PI / 2).[
by RELAT_1:74, XXREAL_1:21;
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:33
.=
rng (cosec | ].0,(PI / 2).[)
by A1, RELAT_1:72
.=
cosec .: ].0,(PI / 2).[
by RELAT_1:115
;
A3: (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) | ].0,(PI / 2).[) " =
((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) "
by RELAT_1:72
.=
arccosec2 | ((cosec | ].0,(PI / 2).]) .: ].0,(PI / 2).[)
by RFUNCT_2:17
.=
arccosec2 | (rng ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[))
by RELAT_1:115
.=
arccosec2 | (rng (cosec | ].0,(PI / 2).[))
by RELAT_1:74, XXREAL_1:21
.=
arccosec2 | (cosec .: ].0,(PI / 2).[)
by RELAT_1:115
;
A4:
(cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[ is_differentiable_on ].0,(PI / 2).[
by A1, Th8, FDIFF_2:16;
now for x0 being Real st x0 in ].0,(PI / 2).[ holds
diff (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[),x0) < 0 A5:
for
x0 being
Real st
x0 in ].0,(PI / 2).[ holds
- ((cos . x0) / ((sin . x0) ^2)) < 0
let x0 be
Real;
( x0 in ].0,(PI / 2).[ implies diff (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[),x0) < 0 )assume A8:
x0 in ].0,(PI / 2).[
;
diff (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[),x0) < 0 diff (
((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[),
x0) =
(((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) `| ].0,(PI / 2).[) . x0
by A4, A8, FDIFF_1:def 7
.=
((cosec | ].0,(PI / 2).[) `| ].0,(PI / 2).[) . x0
by RELAT_1:74, XXREAL_1:21
.=
(cosec `| ].0,(PI / 2).[) . x0
by Th8, FDIFF_2:16
.=
diff (
cosec,
x0)
by A8, Th8, FDIFF_1:def 7
.=
- ((cos . x0) / ((sin . x0) ^2))
by A8, Th8
;
hence
diff (
((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[),
x0)
< 0
by A8, A5;
verum end;
then A9:
arccosec2 | (cosec .: ].0,(PI / 2).[) is_differentiable_on cosec .: ].0,(PI / 2).[
by A2, A4, A3, Lm24, FDIFF_2:48;
A10:
for x being Real st x in cosec .: ].0,(PI / 2).[ holds
arccosec2 | (cosec .: ].0,(PI / 2).[) is_differentiable_in x
cosec .: ].0,(PI / 2).[ c= dom arccosec2
by A2, A3, RELAT_1:60;
hence
arccosec2 is_differentiable_on cosec .: ].0,(PI / 2).[
by A10, FDIFF_1:def 6; verum