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

AA: now

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

proof

let x0 be Real; :: thesis: ( x0 in ].(PI / 2),PI .[ implies (sin . x0) / ((cos . x0) ^2 ) > 0 )
assume A6: x0 in ].(PI / 2),PI .[ ; :: thesis: (sin . x0) / ((cos . x0) ^2 ) > 0
].(PI / 2),PI .[ c= ].0 ,PI .[ by XXREAL_1:46;
then A7: sin . x0 > 0 by A6, COMPTRIG:23;
].(PI / 2),PI .[ c= ].(PI / 2),((3 / 2) * PI ).[ by COMPTRIG:21, XXREAL_1:46;
then cos . x0 < 0 by A6, COMPTRIG:29;
then (cos . x0) ^2 > 0 ;
then (sin . x0) / ((cos . x0) ^2 ) > 0 / ((cos . x0) ^2 ) by A7;
hence (sin . x0) / ((cos . x0) ^2 ) > 0 ; :: thesis: verum

end;

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

end;

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

proof

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

end;

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