set X = sec .: ].(PI / 2),PI.[;
set g1 = arcsec2 | (sec .: ].(PI / 2),PI.[);
set f = sec | ].(PI / 2),PI.];
set g = (sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[;
A1: (sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[ = sec | ].(PI / 2),PI.[ by RELAT_1:74, XXREAL_1:21;
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:33
.= rng (sec | ].(PI / 2),PI.[) by A1, RELAT_1:72
.= sec .: ].(PI / 2),PI.[ by RELAT_1:115 ;
A3: (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) | ].(PI / 2),PI.[) " = ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) " by RELAT_1:72
.= arcsec2 | ((sec | ].(PI / 2),PI.]) .: ].(PI / 2),PI.[) by RFUNCT_2:17
.= arcsec2 | (rng ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[)) by RELAT_1:115
.= arcsec2 | (rng (sec | ].(PI / 2),PI.[)) by RELAT_1:74, XXREAL_1:21
.= arcsec2 | (sec .: ].(PI / 2),PI.[) by RELAT_1:115 ;
A4: (sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[ is_differentiable_on ].(PI / 2),PI.[ by A1, Th6, FDIFF_2:16;

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

A5: 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= ].(PI / 2),((3 / 2) * PI).[ by COMPTRIG:5, XXREAL_1:46;
then A7: cos . x0 < 0 by A6, COMPTRIG:13;
].(PI / 2),PI.[ c= ].0,PI.[ by XXREAL_1:46;
then sin . x0 > 0 by A6, COMPTRIG:7;
hence (sin . x0) / ((cos . x0) ^2) > 0 by A7; :: thesis: verum

end;

let x0 be Real; :: thesis: ( x0 in ].(PI / 2),PI.[ implies diff (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[),x0) > 0 )
assume A8: x0 in ].(PI / 2),PI.[ ; :: thesis: diff (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[),x0) > 0
diff (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[),x0) = (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) `| ].(PI / 2),PI.[) . x0 by A4, A8, FDIFF_1:def 7
.= ((sec | ].(PI / 2),PI.[) `| ].(PI / 2),PI.[) . x0 by RELAT_1:74, XXREAL_1:21
.= (sec `| ].(PI / 2),PI.[) . x0 by Th6, FDIFF_2:16
.= diff (sec,x0) by A8, Th6, FDIFF_1:def 7
.= (sin . x0) / ((cos . x0) ^2) by A8, Th6 ;
hence diff (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[),x0) > 0 by A8, A5; :: thesis: verum

end;

then A9: arcsec2 | (sec .: ].(PI / 2),PI.[) is_differentiable_on sec .: ].(PI / 2),PI.[ by A2, A4, A3, Lm22, FDIFF_2:48;
A10: 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 6;
hence arcsec2 | (sec .: ].(PI / 2),PI.[) is_differentiable_in x by RELAT_1:72; :: thesis: verum

end;

sec .: ].(PI / 2),PI.[ c= dom arcsec2 by A2, A3, RELAT_1:60;
hence arcsec2 is_differentiable_on sec .: ].(PI / 2),PI.[ by A10, FDIFF_1:def 6; :: thesis: verum