:: Inverse Trigonometric Functions Arcsec1, Arcsec2, Arccosec1 and Arccosec2
::  by Bing Xie , Xiquan Liang and Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, REAL_1, XREAL_0, ORDINAL1, SUBSET_1, RCOMP_1, SEQ_1,
      PARTFUN1, XXREAL_1, CARD_1, SIN_COS, ARYTM_3, TARSKI, ARYTM_1, XBOOLE_0,
      RELAT_1, SIN_COS4, ORDINAL4, FUNCT_1, FDIFF_1, SQUARE_1, ORDINAL2,
      XXREAL_0, VALUED_0, FCONT_1, SEQ_2, FUNCT_2, SINCOS10;
 notations TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, RCOMP_1, SIN_COS, RFUNCT_1, SQUARE_1, NUMBERS, REAL_1, SEQ_1,
      FDIFF_1, XREAL_0, INT_1, SIN_COS4, PARTFUN2, RFUNCT_2, FCONT_1, XBOOLE_0,
      FDIFF_9, SEQ_2;
 constructors REAL_1, SQUARE_1, RCOMP_1, RFUNCT_1, FDIFF_1, RFUNCT_2, FCONT_1,
      SIN_COS, PARTFUN2, SIN_COS4, RELSET_1, FDIFF_9, SEQ_1, SEQ_2, XXREAL_2,
      NEWTON, COMSEQ_2;
 registrations XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RELSET_1,
      FUNCT_1, SIN_COS6, RFUNCT_2, ORDINAL1, INT_1, VALUED_0, XXREAL_2,
      XBOOLE_0, NUMBERS;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
 definitions TARSKI, FDIFF_9, XCMPLX_0, RCOMP_1, RFUNCT_2, SQUARE_1;
 theorems SIN_COS6, FDIFF_2, XCMPLX_1, FDIFF_1, RELAT_1, SIN_COS, COMPTRIG,
      RFUNCT_2, FCONT_1, FUNCT_1, XBOOLE_0, SQUARE_1, FCONT_3, XREAL_1, TARSKI,
      XBOOLE_1, ROLLE, RFUNCT_1, FCONT_2, SEQ_1, FDIFF_9, XXREAL_0, FUNCT_2,
      XXREAL_1, XXREAL_2;

begin ::  arcsec, arccosec

reserve x, r for Real,
      th for real number,

  rr for set,

  rseq for Real_Sequence;

Lm1: [.0,PI/2.[ c= ].-PI/2,PI/2.[
proof
A1: 0 in ].-PI/2,PI/2.[;
A2: {0} c= ].-PI/2,PI/2.[
  proof
    let x be set;
    assume x in {0};
    hence thesis by A1,TARSKI:def 1;
  end;
  ].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
  then ].0,PI/2.[ \/ {0} c= ].-PI/2,PI/2.[ by A2,XBOOLE_1:8;
  hence thesis by XXREAL_1:131;
end;

theorem Th1:
  [.0,PI/2.[ c= dom sec
proof
  [.0,PI/2.[ /\ cos"{0} = {}
  proof
    assume [.0,PI/2.[ /\ cos"{0} <> {};
    then consider rr such that
A1: rr in [.0,PI/2.[ /\ cos"{0} by XBOOLE_0:def 1;
    rr in cos"{0} by A1,XBOOLE_0:def 4;
    then
A2: cos.(rr) in {0} by FUNCT_1:def 7;
    rr in [.0,PI/2.[ by A1,XBOOLE_0:def 4;
    then cos.rr <> 0 by Lm1,COMPTRIG:11;
    hence contradiction by A2,TARSKI:def 1;
  end;
  then
  [.0,PI/2.[ \ cos"{0} c= dom cos \ cos"{0} & [.0,PI/2.[ misses cos"{0} by
SIN_COS:24,XBOOLE_0:def 7,XBOOLE_1:33;
  then [.0,PI/2.[ c= dom cos \ cos"{0} by XBOOLE_1:83;
  hence thesis by RFUNCT_1:def 2;
end;

Lm2: ].PI/2,PI.] c= ].PI/2,3/2*PI.[
proof
A1: PI/2 < PI/1 by XREAL_1:76;
A2: PI < 3/2*PI by XREAL_1:155;
  then
A3: PI in ].PI/2,3/2*PI.[ by A1;
A4: {PI} c= ].PI/2,3/2*PI.[
  proof
    let x be set;
    assume x in {PI};
    hence thesis by A3,TARSKI:def 1;
  end;
  ].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by A2,XXREAL_1:46;
  then ].PI/2,PI.[ \/ {PI} c= ].PI/2,3/2*PI.[ by A4,XBOOLE_1:8;
  hence thesis by A1,XXREAL_1:132;
end;

theorem Th2:
  ].PI/2,PI.] c= dom sec
proof
  ].PI/2,PI.] /\ cos"{0} = {}
  proof
    assume ].PI/2,PI.] /\ cos"{0} <> {};
    then consider rr such that
A1: rr in ].PI/2,PI.] /\ cos"{0} by XBOOLE_0:def 1;
    rr in cos"{0} by A1,XBOOLE_0:def 4;
    then
A2: cos.(rr) in {0} by FUNCT_1:def 7;
    rr in ].PI/2,PI.] by A1,XBOOLE_0:def 4;
    then cos.rr <> 0 by Lm2,COMPTRIG:13;
    hence contradiction by A2,TARSKI:def 1;
  end;
  then
  ].PI/2,PI.] \ cos"{0} c= dom cos \ cos"{0} & ].PI/2,PI.] misses cos"{0}
  by SIN_COS:24,XBOOLE_0:def 7,XBOOLE_1:33;
  then ].PI/2,PI.] c= dom cos \ cos"{0} by XBOOLE_1:83;
  hence thesis by RFUNCT_1:def 2;
end;

Lm3: [.-PI/2,0.[ c= ].-PI,0.[
proof
  PI/2 < PI/1 by XREAL_1:76;
  then
A1: -PI < -PI/2 by XREAL_1:24;
  then
A2: -PI/2 in ].-PI,0.[;
A3: {-PI/2} c= ].-PI,0.[
  proof
    let x be set;
    assume x in {-PI/2};
    hence thesis by A2,TARSKI:def 1;
  end;
  ].-PI/2,0.[ c= ].-PI,0.[ by A1,XXREAL_1:46;
  then ].-PI/2,0.[ \/ {-PI/2} c= ].-PI,0.[ by A3,XBOOLE_1:8;
  hence thesis by XXREAL_1:131;
end;

theorem Th3:
  [.-PI/2,0.[ c= dom cosec
proof
  [.-PI/2,0.[ /\ sin"{0} = {}
  proof
    assume [.-PI/2,0.[ /\ sin"{0} <> {};
    then consider rr such that
A1: rr in [.-PI/2,0.[ /\ sin"{0} by XBOOLE_0:def 1;
A2: rr in sin"{0} by A1,XBOOLE_0:def 4;
A3: rr in [.-PI/2,0.[ by A1,XBOOLE_0:def 4;
    reconsider rr as real number by A1;
    rr < 0 by A3,Lm3,XXREAL_1:4;
    then
A4: rr+2*PI < 0+2*PI by XREAL_1:8;
    -PI < rr by A3,Lm3,XXREAL_1:4;
    then -PI+2*PI < rr+2*PI by XREAL_1:8;
    then rr+2*PI in ].PI,2*PI.[ by A4;
    then sin.(rr+2*PI) < 0 by COMPTRIG:9;
    then
A5: sin.rr <> 0 by SIN_COS:78;
    sin.rr in {0} by A2,FUNCT_1:def 7;
    hence contradiction by A5,TARSKI:def 1;
  end;
  then
  [.-PI/2,0.[ \ sin"{0} c= dom sin \ sin"{0} & [.-PI/2,0.[ misses sin"{0}
  by SIN_COS:24,XBOOLE_0:def 7,XBOOLE_1:33;
  then [.-PI/2,0.[ c= dom sin \ sin"{0} by XBOOLE_1:83;
  hence thesis by RFUNCT_1:def 2;
end;

Lm4: ].0,PI/2.] c= ].0,PI.[
proof
A1: PI/2 < PI/1 by XREAL_1:76;
  then
A2: PI/2 in ].0,PI.[;
A3: {PI/2} c= ].0,PI.[
  proof
    let x be set;
    assume x in {PI/2};
    hence thesis by A2,TARSKI:def 1;
  end;
  ].0,PI/2.[ c= ].0,PI.[ by A1,XXREAL_1:46;
  then ].0,PI/2.[ \/ {PI/2} c= ].0,PI.[ by A3,XBOOLE_1:8;
  hence thesis by XXREAL_1:132;
end;

theorem Th4:
  ].0,PI/2.] c= dom cosec
proof
  ].0,PI/2.] /\ sin"{0} = {}
  proof
    assume ].0,PI/2.] /\ sin"{0} <> {};
    then consider rr such that
A1: rr in ].0,PI/2.] /\ sin"{0} by XBOOLE_0:def 1;
    rr in sin"{0} by A1,XBOOLE_0:def 4;
    then
A2: sin.rr in {0} by FUNCT_1:def 7;
    rr in ].0,PI/2.] by A1,XBOOLE_0:def 4;
    then sin.rr <> 0 by Lm4,COMPTRIG:7;
    hence contradiction by A2,TARSKI:def 1;
  end;
  then
  ].0,PI/2.] \ sin"{0} c= dom sin \ sin"{0} & ].0,PI/2.] misses sin"{0} by
SIN_COS:24,XBOOLE_0:def 7,XBOOLE_1:33;
  then ].0,PI/2.] c= dom sin \ sin"{0} by XBOOLE_1:83;
  hence thesis by RFUNCT_1:def 2;
end;

theorem Th5:
  sec is_differentiable_on ].0,PI/2.[ & for x st x in ].0,PI/2.[
  holds diff(sec,x) = sin.x/(cos.x)^2
proof
  set Z = ].0,PI/2.[;
  [.0,PI/2.[ = Z \/ {0} by XXREAL_1:131;
  then Z c= [.0,PI/2.[ by XBOOLE_1:7;
  then
A1: Z c= dom sec by Th1,XBOOLE_1:1;
  then
A2: sec is_differentiable_on Z by FDIFF_9:4;
  for x st x in Z holds diff(sec,x) = sin.x/(cos.x)^2
  proof
    let x;
    assume
A3: x in Z;
    then diff(sec,x) = ((sec)`|Z).x by A2,FDIFF_1:def 7
      .= sin.x/(cos.x)^2 by A1,A3,FDIFF_9:4;
    hence thesis;
  end;
  hence thesis by A1,FDIFF_9:4;
end;

theorem Th6:
  sec is_differentiable_on ].PI/2,PI.[ & for x st x in ].PI/2,PI.[
  holds diff(sec,x) = sin.x/(cos.x)^2
proof
  set Z = ].PI/2,PI.[;
  PI/2 < PI/1 by XREAL_1:76;
  then ].PI/2,PI.] = Z \/ {PI} by XXREAL_1:132;
  then Z c= ].PI/2,PI.] by XBOOLE_1:7;
  then
A1: Z c= dom sec by Th2,XBOOLE_1:1;
  then
A2: sec is_differentiable_on Z by FDIFF_9:4;
  for x st x in Z holds diff(sec,x) = sin.x/(cos.x)^2
  proof
    let x;
    assume
A3: x in Z;
    then diff(sec,x) = ((sec)`|Z).x by A2,FDIFF_1:def 7
      .= sin.x/(cos.x)^2 by A1,A3,FDIFF_9:4;
    hence thesis;
  end;
  hence thesis by A1,FDIFF_9:4;
end;

theorem Th7:
  cosec is_differentiable_on ].-PI/2,0.[ & for x st x in ].-PI/2,0
  .[ holds diff(cosec,x) = -cos.x/(sin.x)^2
proof
  set Z = ].-PI/2,0.[;
  [.-PI/2,0.[ = Z \/ {-PI/2} by XXREAL_1:131;
  then Z c= [.-PI/2,0.[ by XBOOLE_1:7;
  then
A1: Z c= dom cosec by Th3,XBOOLE_1:1;
  then
A2: cosec is_differentiable_on Z by FDIFF_9:5;
  for x st x in Z holds diff(cosec,x) = -cos.x/(sin.x)^2
  proof
    let x;
    assume
A3: x in Z;
    then diff(cosec,x) = ((cosec)`|Z).x by A2,FDIFF_1:def 7
      .= -cos.x/(sin.x)^2 by A1,A3,FDIFF_9:5;
    hence thesis;
  end;
  hence thesis by A1,FDIFF_9:5;
end;

theorem Th8:
  cosec is_differentiable_on ].0,PI/2.[ & for x st x in ].0,PI/2.[
  holds diff(cosec,x) = -cos.x/(sin.x)^2
proof
  set Z = ].0,PI/2.[;
  ].0,PI/2.] = Z \/ {PI/2} by XXREAL_1:132;
  then Z c= ].0,PI/2.] by XBOOLE_1:7;
  then
A1: Z c= dom cosec by Th4,XBOOLE_1:1;
  then
A2: cosec is_differentiable_on Z by FDIFF_9:5;
  for x st x in Z holds diff(cosec,x) = -cos.x/(sin.x)^2
  proof
    let x;
    assume
A3: x in Z;
    then diff(cosec,x) = ((cosec)`|Z).x by A2,FDIFF_1:def 7
      .= -cos.x/(sin.x)^2 by A1,A3,FDIFF_9:5;
    hence thesis;
  end;
  hence thesis by A1,FDIFF_9:5;
end;

theorem
  sec|].0,PI/2.[ is continuous by Th5,FDIFF_1:25;

theorem
  sec|].PI/2,PI.[ is continuous by Th6,FDIFF_1:25;

theorem
  cosec|].-PI/2,0.[ is continuous by Th7,FDIFF_1:25;

theorem
  cosec|].0,PI/2.[ is continuous by Th8,FDIFF_1:25;

Lm5: 0 in [.0,PI/2.[ & PI/4 in [.0,PI/2.[
proof
  PI/4 < PI/2 by XREAL_1:76;
  hence thesis;
end;

Lm6: 3/4*PI in ].PI/2,PI.] & PI in ].PI/2,PI.]
proof
  PI/4 < PI/2 by XREAL_1:76;
  then PI/4+PI/2 > 0+PI/2 & PI/4+PI/2 < PI/2+PI/2 by XREAL_1:8;
  hence thesis by COMPTRIG:5;
end;

Lm7: -PI/2 in [.-PI/2,0.[ & -PI/4 in [.-PI/2,0.[
proof
  PI/4 < PI/2 by XREAL_1:76;
  then -PI/4 > -PI/2 by XREAL_1:24;
  hence thesis;
end;

Lm8: PI/4 in ].0,PI/2.] & PI/2 in ].0,PI/2.]
proof
  PI/4 < PI/2 by XREAL_1:76;
  hence thesis;
end;

Lm9: ].0,PI/2.[ c= [.0,PI/2.[ by XXREAL_1:22;
then

Lm10: ].0,PI/2.[ c= dom sec by Th1,XBOOLE_1:1;

Lm11: ].PI/2,PI.[ c= ].PI/2,PI.] by XXREAL_1:21;
then

Lm12: ].PI/2,PI.[ c= dom sec by Th2,XBOOLE_1:1;

Lm13: [.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;

Lm14: [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;

Lm15: ].-PI/2,0.[ c= [.-PI/2,0.[ by XXREAL_1:22;
then

Lm16: ].-PI/2,0.[ c= dom cosec by Th3,XBOOLE_1:1;

Lm17: ].0,PI/2.[ c= ].0,PI/2.] by XXREAL_1:21;
then

Lm18: ].0,PI/2.[ c= dom cosec by Th4,XBOOLE_1:1;

Lm19: [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;

Lm20: [.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;

].0,PI/2.[ = dom(sec|].0,PI/2.[) by Lm9,Th1,RELAT_1:62,XBOOLE_1:1;
then

Lm21: ].0,PI/2.[ c= dom(sec|[.0,PI/2.[|].0,PI/2.[) by RELAT_1:74,XXREAL_1:22;

].PI/2,PI.[ = dom(sec|].PI/2,PI.[) by Lm11,Th2,RELAT_1:62,XBOOLE_1:1;
then

Lm22: ].PI/2,PI.[ c= dom(sec|].PI/2,PI.]|].PI/2,PI.[) by RELAT_1:74,XXREAL_1:21
;

].-PI/2,0.[ = dom(cosec|].-PI/2,0.[) by Lm15,Th3,RELAT_1:62,XBOOLE_1:1;
then

Lm23: ].-PI/2,0.[ c= dom(cosec|[.-PI/2,0.[|].-PI/2,0.[) by RELAT_1:74
,XXREAL_1:22;

].0,PI/2.[ = dom(cosec|].0,PI/2.[) by Lm17,Th4,RELAT_1:62,XBOOLE_1:1;
then

Lm24: ].0,PI/2.[ c= dom(cosec|].0,PI/2.]|].0,PI/2.[) by RELAT_1:74,XXREAL_1:21
;

theorem Th13:
  sec|].0,PI/2.[ is increasing
proof
  for x be Real st x in ].0,PI/2.[ holds diff(sec,x) > 0
  proof
    let x be Real;
    assume
A1: x in ].0,PI/2.[;
    ].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
    then
A2: cos.x > 0 by A1,COMPTRIG:11;
    PI/2 < PI/1 by XREAL_1:76;
    then ].0,PI/2.[ c= ].0,PI.[ by XXREAL_1:46;
    then sin.x > 0 by A1,COMPTRIG:7;
    then sin.x/(cos.x)^2 > 0/(cos.x)^2 by A2;
    hence thesis by A1,Th5;
  end;
  hence thesis by Lm9,Th1,Th5,ROLLE:9,XBOOLE_1:1;
end;

theorem Th14:
  sec|].PI/2,PI.[ is increasing
proof
  for x be Real st x in ].PI/2,PI.[ holds diff(sec,x) > 0
  proof
    let x be Real;
    assume
A1: x in ].PI/2,PI.[;
    PI <= 3/2*PI by XREAL_1:151;
    then ].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by XXREAL_1:46;
    then
A2: cos.x < 0 by A1,COMPTRIG:13;
    ].PI/2,PI.[ c= ].0,PI.[ by XXREAL_1:46;
    then sin.x > 0 by A1,COMPTRIG:7;
    then sin.x/(cos.x)^2 > 0/(cos.x)^2 by A2;
    hence thesis by A1,Th6;
  end;
  hence thesis by Lm11,Th2,Th6,ROLLE:9,XBOOLE_1:1;
end;

theorem Th15:
  cosec|].-PI/2,0.[ is decreasing
proof
  for x be Real st x in ].-PI/2,0.[ holds diff(cosec,x) < 0
  proof
    let x be Real;
    assume
A1: x in ].-PI/2,0.[;
    then x < 0 by XXREAL_1:4;
    then
A2: x+2*PI < 0+2*PI by XREAL_1:8;
    ].-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 < x by A1,XXREAL_1:4;
    then -PI+2*PI < x+2*PI by XREAL_1:8;
    then x+2*PI in ].PI,2*PI.[ by A2;
    then sin.(x+2*PI) < 0 by COMPTRIG:9;
    then
A3: sin.x < 0 by SIN_COS:78;
    ].-PI/2,0.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
    then cos.x > 0 by A1,COMPTRIG:11;
    then -cos.x/(sin.x)^2 < -0 by A3;
    hence thesis by A1,Th7;
  end;
  hence thesis by Lm15,Th3,Th7,ROLLE:10,XBOOLE_1:1;
end;

theorem Th16:
  cosec|].0,PI/2.[ is decreasing
proof
  for x be Real st x in ].0,PI/2.[ holds diff(cosec,x) < 0
  proof
    let x be Real;
    assume
A1: x in ].0,PI/2.[;
    ].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
    then
A2: cos.x > 0 by A1,COMPTRIG:11;
    ].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:5,XXREAL_1:46;
    then sin.x > 0 by A1,COMPTRIG:7;
    then -cos.x/(sin.x)^2 < -0 by A2;
    hence thesis by A1,Th8;
  end;
  hence thesis by Lm17,Th4,Th8,ROLLE:10,XBOOLE_1:1;
end;

theorem Th17:
  sec|[.0,PI/2.[ is increasing
proof
  now
    let r1,r2 be Real;
    assume that
A1: r1 in [.0,PI/2.[ /\ dom sec and
A2: r2 in [.0,PI/2.[ /\ dom sec and
A3: r1 < r2;
A4: r1 in dom sec by A1,XBOOLE_0:def 4;
A5: r1 in [.0,PI/2.[ by A1,XBOOLE_0:def 4;
    then
A6: r1 < PI/2 by XXREAL_1:3;
A7: r2 in dom sec by A2,XBOOLE_0:def 4;
A8: r2 in [.0,PI/2.[ by A2,XBOOLE_0:def 4;
    then
A9: r2 < PI/2 by XXREAL_1:3;
    now
      per cases by A5,XXREAL_1:3;
      suppose
A10:    0 = r1;
        r2 < PI/2 & PI/2 < 2*PI by A8,Lm1,XREAL_1:68,XXREAL_1:4;
        then r2 < 2*PI by XXREAL_0:2;
        then cos r2 < 1 by A3,A10,SIN_COS6:34;
        then
A11:    cos.r2 < 1 by SIN_COS:def 19;
        -PI/2+2*PI*0 < r2 & r2 < PI/2+2*PI*0 by A8,Lm1,XXREAL_1:4;
        then cos r2 > 0 by SIN_COS6:13;
        then cos.r2 > 0 by SIN_COS:def 19;
        then
A12:    1/1 < 1/cos.r2 by A11,XREAL_1:76;
        sec.r1 = 1/1 by A4,A10,RFUNCT_1:def 2,SIN_COS:30
          .= 1;
        hence sec.r2 > sec.r1 by A7,A12,RFUNCT_1:def 2;
      end;
      suppose
A13:    0 < r1;
        then r1 in ].0,PI/2.[ by A6;
        then
A14:    r1 in ].0,PI/2.[ /\ dom sec by A4,XBOOLE_0:def 4;
        r2 in ].0,PI/2.[ by A3,A9,A13;
        then r2 in ].0,PI/2.[ /\ dom sec by A7,XBOOLE_0:def 4;
        hence sec.r2 > sec.r1 by A3,A14,Th13,RFUNCT_2:20;
      end;
    end;
    hence sec.r2 > sec.r1;
  end;
  hence thesis by RFUNCT_2:20;
end;

theorem Th18:
  sec|].PI/2,PI.] is increasing
proof
  now
    let r1,r2 be Real;
    assume that
A1: r1 in ].PI/2,PI.] /\ dom sec and
A2: r2 in ].PI/2,PI.] /\ dom sec and
A3: r1 < r2;
A4: r1 in dom sec by A1,XBOOLE_0:def 4;
A5: r2 in dom sec by A2,XBOOLE_0:def 4;
A6: r1 in ].PI/2,PI.] by A1,XBOOLE_0:def 4;
    then
A7: PI/2 < r1 by XXREAL_1:2;
A8: r2 in ].PI/2,PI.] by A2,XBOOLE_0:def 4;
    then
A9: r2 <= PI by XXREAL_1:2;
A10: PI/2 < r2 by A8,XXREAL_1:2;
    now
      per cases by A9,XXREAL_0:1;
      suppose
A11:    r2 < PI;
        then r1 < PI by A3,XXREAL_0:2;
        then r1 in ].PI/2,PI.[ by A7;
        then
A12:    r1 in ].PI/2,PI.[ /\ dom sec by A4,XBOOLE_0:def 4;
        r2 in ].PI/2,PI.[ by A10,A11;
        then r2 in ].PI/2,PI.[ /\ dom sec by A5,XBOOLE_0:def 4;
        hence sec.r2 > sec.r1 by A3,A12,Th14,RFUNCT_2:20;
      end;
      suppose
A13:    r2 = PI;
        PI*1 < PI*(3/2) by XREAL_1:68;
        then
A14:    r1 < 3/2*PI+2*PI*0 by A3,A13,XXREAL_0:2;
        PI/2+2*PI*0 < r1 by A6,XXREAL_1:2;
        then cos r1 < 0 by A14,SIN_COS6:14;
        then
A15:    cos.r1 < 0 by SIN_COS:def 19;
        r1 < PI by A3,A9,XXREAL_0:2;
        then cos r1 > -1 by A7,SIN_COS6:35;
        then cos.r1 > -1 by SIN_COS:def 19;
        then
A16:    (cos.r1)" < (-1)" by A15,XREAL_1:87;
        sec.r2 = 1/(-1) by A5,A13,RFUNCT_1:def 2,SIN_COS:76
          .= -1;
        hence sec.r1 < sec.r2 by A4,A16,RFUNCT_1:def 2;
      end;
    end;
    hence sec.r2 > sec.r1;
  end;
  hence thesis by RFUNCT_2:20;
end;

theorem Th19:
  cosec|[.-PI/2,0.[ is decreasing
proof
  now
    let r1,r2 be Real;
    assume that
A1: r1 in [.-PI/2,0.[ /\ dom cosec and
A2: r2 in [.-PI/2,0.[ /\ dom cosec and
A3: r1 < r2;
A4: r1 in dom cosec by A1,XBOOLE_0:def 4;
A5: r1 in [.-PI/2,0.[ by A1,XBOOLE_0:def 4;
    then
A6: r1 < 0 by XXREAL_1:3;
A7: r2 in dom cosec by A2,XBOOLE_0:def 4;
A8: r2 in [.-PI/2,0.[ by A2,XBOOLE_0:def 4;
    then
A9: r2 < 0 by XXREAL_1:3;
A10: -PI/2 <= r1 by A5,XXREAL_1:3;
    now
      per cases by A10,XXREAL_0:1;
      suppose
A11:    -PI/2 = r1;
        -PI/2 > -PI by COMPTRIG:5,XREAL_1:24;
        then
A12:    ].-PI/2,0.[ c= ].-PI,0.[ by XXREAL_1:46;
        r2 in ].-PI/2,0.[ by A3,A9,A11;
        then -PI < r2 by A12,XXREAL_1:4;
        then
A13:    -PI+2*PI < r2+2*PI by XREAL_1:8;
        r2+2*PI < 0+2*PI by A9,XREAL_1:8;
        then r2+2*PI in ].PI,2*PI.[ by A13;
        then sin.(r2+2*PI) < 0 by COMPTRIG:9;
        then
A14:    sin.r2 < 0 by SIN_COS:78;
A15:    r2 < 2*PI+2*PI*(-1) by A8,XXREAL_1:3;
        3/2*PI+2*PI*(-1) < r2 by A3,A11;
        then sin r2 > -1 by A15,SIN_COS6:39;
        then sin.r2 > -1 by SIN_COS:def 17;
        then
A16:    (sin.r2)" < (-1)" by A14,XREAL_1:87;
        cosec.r1 = 1/sin.(-PI/2) by A4,A11,RFUNCT_1:def 2
          .= 1/(-1) by SIN_COS:30,76
          .= -1;
        hence cosec.r2 < cosec.r1 by A7,A16,RFUNCT_1:def 2;
      end;
      suppose
A17:    -PI/2 < r1;
        then -PI/2 < r2 by A3,XXREAL_0:2;
        then r2 in ].-PI/2,0.[ by A9;
        then
A18:    r2 in ].-PI/2,0.[ /\ dom cosec by A7,XBOOLE_0:def 4;
        r1 in ].-PI/2,0.[ by A6,A17;
        then r1 in ].-PI/2,0.[ /\ dom cosec by A4,XBOOLE_0:def 4;
        hence cosec.r2 < cosec.r1 by A3,A18,Th15,RFUNCT_2:21;
      end;
    end;
    hence cosec.r2 < cosec.r1;
  end;
  hence thesis by RFUNCT_2:21;
end;

theorem Th20:
  cosec|].0,PI/2.] is decreasing
proof
  now
    let r1,r2 be Real;
    assume that
A1: r1 in ].0,PI/2.] /\ dom cosec and
A2: r2 in ].0,PI/2.] /\ dom cosec and
A3: r1 < r2;
A4: r1 in dom cosec by A1,XBOOLE_0:def 4;
A5: r2 in ].0,PI/2.] by A2,XBOOLE_0:def 4;
    then
A6: r2 <= PI/2 by XXREAL_1:2;
A7: r2 in dom cosec by A2,XBOOLE_0:def 4;
A8: r1 in ].0,PI/2.] by A1,XBOOLE_0:def 4;
    then
A9: 0 < r1 by XXREAL_1:2;
A10: 0 < r2 by A5,XXREAL_1:2;
    now
      per cases by A6,XXREAL_0:1;
      suppose
A11:    r2 < PI/2;
        then r1 < PI/2 by A3,XXREAL_0:2;
        then r1 in ].0,PI/2.[ by A9;
        then
A12:    r1 in ].0,PI/2.[ /\ dom cosec by A4,XBOOLE_0:def 4;
        r2 in ].0,PI/2.[ by A10,A11;
        then r2 in ].0,PI/2.[ /\ dom cosec by A7,XBOOLE_0:def 4;
        hence cosec.r2 < cosec.r1 by A3,A12,Th16,RFUNCT_2:21;
      end;
      suppose
A13:    r2 = PI/2;
        then sin r1 < 1 by A3,A9,SIN_COS6:30;
        then
A14:    sin.r1 < 1 by SIN_COS:def 17;
        sin.r1 > 0 by A8,Lm4,COMPTRIG:7;
        then
A15:    1/1 < 1/sin.r1 by A14,XREAL_1:76;
        cosec.r2 = 1/1 by A7,A13,RFUNCT_1:def 2,SIN_COS:76
          .= 1;
        hence cosec.r2 < cosec.r1 by A4,A15,RFUNCT_1:def 2;
      end;
    end;
    hence cosec.r2 < cosec.r1;
  end;
  hence thesis by RFUNCT_2:21;
end;

theorem
  sec | [.0,PI/2.[ is one-to-one by Th17,FCONT_3:8;

theorem
  sec | ].PI/2,PI.] is one-to-one by Th18,FCONT_3:8;

theorem
  cosec | [.-PI/2,0.[ is one-to-one by Th19,FCONT_3:8;

theorem
  cosec | ].0,PI/2.] is one-to-one by Th20,FCONT_3:8;

registration
  cluster sec | [.0,PI/2.[ -> one-to-one;
  coherence by Th17,FCONT_3:8;
  cluster sec | ].PI/2,PI.] -> one-to-one;
  coherence by Th18,FCONT_3:8;
  cluster cosec | [.-PI/2,0.[ -> one-to-one;
  coherence by Th19,FCONT_3:8;
  cluster cosec | ].0,PI/2.] -> one-to-one;
  coherence by Th20,FCONT_3:8;
end;

definition
  func arcsec1 -> PartFunc of REAL, REAL equals
  (sec | [.0,PI/2.[)";
  coherence;
  func arcsec2 -> PartFunc of REAL, REAL equals
  (sec | ].PI/2, PI.])";
  coherence;
  func arccosec1 -> PartFunc of REAL, REAL equals
  (cosec | [.-PI/2,0.[)";
  coherence;
  func arccosec2 -> PartFunc of REAL, REAL equals
  (cosec | ].0,PI/2.])";
  coherence;
end;

definition
  let r be Real;
  func arcsec1 r equals
  arcsec1.r;
  coherence;
  func arcsec2 r equals
  arcsec2.r;
  coherence;
  func arccosec1 r equals
  arccosec1.r;
  coherence;
  func arccosec2 r equals
  arccosec2.r;
  coherence;
end;

definition
  let r be Real;
  redefine func arcsec1 r -> Real;
  coherence;
  redefine func arcsec2 r -> Real;
  coherence;
  redefine func arccosec1 r -> Real;
  coherence;
  redefine func arccosec2 r -> Real;
  coherence;
end;

Lm25: (arcsec1 qua Function)" = sec | [.0,PI/2.[ by FUNCT_1:43;

Lm26: (arcsec2 qua Function)" = sec | ].PI/2,PI.] by FUNCT_1:43;

Lm27: (arccosec1 qua Function)" = cosec | [.-PI/2,0.[ by FUNCT_1:43;

Lm28: (arccosec2 qua Function)" = cosec | ].0,PI/2.] by FUNCT_1:43;

theorem Th25:
  rng arcsec1 = [.0,PI/2.[
proof
  dom (sec|[.0,PI/2.[) = [.0,PI/2.[ by Th1,RELAT_1:62;
  hence thesis by FUNCT_1:33;
end;

theorem Th26:
  rng arcsec2 = ].PI/2,PI.]
proof
  dom (sec|].PI/2,PI.]) = ].PI/2,PI.] by Th2,RELAT_1:62;
  hence thesis by FUNCT_1:33;
end;

theorem Th27:
  rng arccosec1 = [.-PI/2,0.[
proof
  dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ by Th3,RELAT_1:62;
  hence thesis by FUNCT_1:33;
end;

theorem Th28:
  rng arccosec2 = ].0,PI/2.]
proof
  dom (cosec|].0,PI/2.]) = ].0,PI/2.] by Th4,RELAT_1:62;
  hence thesis by FUNCT_1:33;
end;

registration
  cluster arcsec1 -> one-to-one;
  coherence;
  cluster arcsec2 -> one-to-one;
  coherence;
  cluster arccosec1 -> one-to-one;
  coherence;
  cluster arccosec2 -> one-to-one;
  coherence;
end;

theorem Th29:
  sin.(PI/4) = 1/sqrt 2 & cos.(PI/4) = 1/sqrt 2
proof
A1: (sqrt(1/2))^2 = 1/2 by SQUARE_1:def 2;
  1 = (sin.(PI/4))^2 + (sin.(PI/4))^2 by SIN_COS:28,73
    .= 2*(sin.(PI/4))^2;
  then
A2: sin.(PI/4) = sqrt(1/2) or sin.(PI/4) = -sqrt(1/2) by A1,SQUARE_1:40;
  PI/4 < PI/1 by XREAL_1:76;
  then
A3: PI/4 in ].0,PI.[;
  sqrt(1/2) > 0 by SQUARE_1:25;
  hence thesis by A2,A3,COMPTRIG:7,SIN_COS:73,SQUARE_1:32;
end;

theorem Th30:
  sin.(-PI/4) = -1/sqrt 2 & cos.(-PI/4) = 1/sqrt 2 & sin.(3/4*PI)
  = 1/sqrt 2 & cos.(3/4*PI) = -1/sqrt 2
proof
A1: cos.(-PI/4) = 1/sqrt 2 by Th29,SIN_COS:30;
A2: cos.(3/4*PI) = cos.(PI+(-PI/4)) .= -1/sqrt 2 by A1,SIN_COS:78;
A3: sin.(-PI/4) = -1/sqrt 2 by Th29,SIN_COS:30;
  sin.(3/4*PI) = sin.(PI+(-PI/4)) .= -(-1/sqrt 2) by A3,SIN_COS:78
    .= 1/sqrt 2;
  hence thesis by A2,Th29,SIN_COS:30;
end;

theorem Th31:
  sec.0 = 1 & sec.(PI/4) = sqrt 2 & sec.(3/4*PI) = -sqrt 2 & sec. PI = -1
proof
A1: sec.PI = 1/(-1) by Lm6,Th2,RFUNCT_1:def 2,SIN_COS:76
    .= -1;
A2: sec.(3/4*PI) = 1/(-1/sqrt 2) by Lm6,Th2,Th30,RFUNCT_1:def 2
    .= -1/(1/sqrt 2) by XCMPLX_1:188
    .= -sqrt 2;
A3: sec.0 = 1/1 by Lm5,Th1,RFUNCT_1:def 2,SIN_COS:30
    .= 1;
  sec.(PI/4) = 1/(1/sqrt 2) by Lm5,Th1,Th29,RFUNCT_1:def 2
    .= sqrt 2;
  hence thesis by A3,A2,A1;
end;

theorem Th32:
  cosec.(-PI/2) = -1 & cosec.(-PI/4) = -sqrt 2 & cosec.(PI/4) =
  sqrt 2 & cosec.(PI/2) = 1
proof
A1: cosec.(PI/2) = 1/1 by Lm8,Th4,RFUNCT_1:def 2,SIN_COS:76
    .= 1;
A2: cosec.(PI/4) = 1/(1/sqrt 2) by Lm8,Th4,Th29,RFUNCT_1:def 2
    .= sqrt 2;
A3: cosec.(-PI/2) = 1/sin.(-PI/2) by Lm7,Th3,RFUNCT_1:def 2
    .= 1/(-1) by SIN_COS:30,76
    .= -1;
  cosec.(-PI/4) = 1/(-1/sqrt 2) by Lm7,Th3,Th30,RFUNCT_1:def 2
    .= -1/(1/sqrt 2) by XCMPLX_1:188
    .= -sqrt 2;
  hence thesis by A3,A2,A1;
end;

theorem Th33:
  for x be set st x in [.0,PI/4.] holds sec.x in [.1,sqrt 2.]
proof
  let x be set;
  assume x in [.0,PI/4.];
  then x in ].0,PI/4.[ \/ {0,PI/4} by XXREAL_1:128;
  then
A1: x in ].0,PI/4.[ or x in {0,PI/4} by XBOOLE_0:def 3;
  per cases by A1,TARSKI:def 2;
  suppose
A2: x in ].0,PI/4.[;
    PI/4 < PI/2 by XREAL_1:76;
    then 0 in [.0,PI/2.[ & PI/4 in [.0,PI/2.[;
    then
A3: [.0,PI/4.] c= [.0,PI/2.[ by XXREAL_2:def 12;
    then
A4: sec|[.0,PI/4.] is increasing by Th17,RFUNCT_2:28;
A5: ex s be Real st s=x & 0 < s & s < PI/4 by A2;
A6: ].0,PI/4.[ c= [.0,PI/4.] by XXREAL_1:25;
A7: [.0,PI/4.] /\ dom sec = [.0,PI/4.] by A3,Th1,XBOOLE_1:1,28;
    0 in [.0,PI/4.] & ex s be Real st s=x & 0 < s & s < PI/4 by A2;
    then
A8: 1 < sec.x by A2,A4,A7,A6,Th31,RFUNCT_2:20;
    PI/4 in [.0,PI/4.] /\ dom sec by A7;
    then sec.x < sqrt 2 by A2,A4,A7,A6,A5,Th31,RFUNCT_2:20;
    hence thesis by A8;
  end;
  suppose
    x = 0;
    hence thesis by Th31,SQUARE_1:19;
  end;
  suppose
    x = PI/4;
    hence thesis by Th31,SQUARE_1:19;
  end;
end;

theorem Th34:
  for x be set st x in [.3/4*PI,PI.] holds sec.x in [.-sqrt 2,-1.]
proof
  let x be set;
A1: PI/4 < PI/2 by XREAL_1:76;
  then
A2: PI/4+PI/2 < PI/2+PI/2 by XREAL_1:8;
  assume x in [.3/4*PI,PI.];
  then x in ].3/4*PI,PI.[ \/ {3/4*PI,PI} by A2,XXREAL_1:128;
  then
A3: x in ].3/4*PI,PI.[ or x in {3/4*PI,PI} by XBOOLE_0:def 3;
  per cases by A3,TARSKI:def 2;
  suppose
A4: x in ].3/4*PI,PI.[;
    PI/4+PI/4 < PI/2+PI/4 by A1,XREAL_1:8;
    then
A5: 3/4*PI in ].PI/2,PI.] by A2;
    PI in ].PI/2,PI.] by COMPTRIG:5;
    then
A6: [.3/4*PI,PI.] c= ].PI/2,PI.] by A5,XXREAL_2:def 12;
    then
A7: sec|[.3/4*PI,PI.] is increasing by Th18,RFUNCT_2:28;
A8: ex s be Real st s=x & 3/4*PI < s & s < PI by A4;
A9: ex s be Real st s=x & 3/4*PI < s & s < PI by A4;
A10: ].3/4*PI,PI.[ c= [.3/4*PI,PI.] by XXREAL_1:25;
A11: [.3/4*PI,PI.] /\ dom sec = [.3/4*PI,PI.] by A6,Th2,XBOOLE_1:1,28;
    then PI in [.3/4*PI,PI.] /\ dom sec by A2;
    then
A12: sec.x < -1 by A4,A7,A11,A10,A9,Th31,RFUNCT_2:20;
    3/4*PI in [.3/4*PI,PI.] by A2;
    then -sqrt 2 < sec.x by A4,A7,A11,A10,A8,Th31,RFUNCT_2:20;
    hence thesis by A12;
  end;
  suppose
A13: x = 3/4*PI;
    -sqrt 2 < -1 by SQUARE_1:19,XREAL_1:24;
    hence thesis by A13,Th31;
  end;
  suppose
A14: x = PI;
    -sqrt 2 < -1 by SQUARE_1:19,XREAL_1:24;
    hence thesis by A14,Th31;
  end;
end;

theorem Th35:
  for x be set st x in [.-PI/2,-PI/4.] holds cosec.x in [.-sqrt 2, -1.]
proof
  let x be set;
  PI/4 < PI/2 by XREAL_1:76;
  then
A1: -PI/2 < -PI/4 by XREAL_1:24;
  assume x in [.-PI/2,-PI/4.];
  then x in ].-PI/2,-PI/4.[ \/ {-PI/2,-PI/4} by A1,XXREAL_1:128;
  then
A2: x in ].-PI/2,-PI/4.[ or x in {-PI/2,-PI/4} by XBOOLE_0:def 3;
  per cases by A2,TARSKI:def 2;
  suppose
A3: x in ].-PI/2,-PI/4.[;
    then
A4: ex s be Real st s=x & -PI/2 < s & s < -PI/4;
A5: ex s be Real st s=x & -PI/2 < s & s < -PI/4 by A3;
A6: ].-PI/2,-PI/4.[ c= [.-PI/2,-PI/4.] by XXREAL_1:25;
    -PI/2 in [.-PI/2,0.[ & -PI/4 in [.-PI/2,0.[ by A1;
    then
A7: [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by XXREAL_2:def 12;
    then
A8: cosec|[.-PI/2,-PI/4.] is decreasing by Th19,RFUNCT_2:29;
A9: [.-PI/2,-PI/4.] /\ dom cosec = [.-PI/2,-PI/4.] by A7,Th3,XBOOLE_1:1,28;
    then -PI/4 in [.-PI/2,-PI/4.] /\ dom cosec by A1;
    then
A10: cosec.x > -sqrt 2 by A3,A8,A9,A6,A5,Th32,RFUNCT_2:21;
    -PI/2 in [.-PI/2,-PI/4.] by A1;
    then -1 > cosec.x by A3,A8,A9,A6,A4,Th32,RFUNCT_2:21;
    hence thesis by A10;
  end;
  suppose
A11: x = -PI/2;
    -sqrt 2 < -1 by SQUARE_1:19,XREAL_1:24;
    hence thesis by A11,Th32;
  end;
  suppose
A12: x = -PI/4;
    -sqrt 2 < -1 by SQUARE_1:19,XREAL_1:24;
    hence thesis by A12,Th32;
  end;
end;

theorem Th36:
  for x be set st x in [.PI/4,PI/2.] holds cosec.x in [.1,sqrt 2.]
proof
  let x be set;
A1: PI/4 < PI/2 by XREAL_1:76;
  assume x in [.PI/4,PI/2.];
  then x in ].PI/4,PI/2.[ \/ {PI/4,PI/2} by A1,XXREAL_1:128;
  then
A2: x in ].PI/4,PI/2.[ or x in {PI/4,PI/2} by XBOOLE_0:def 3;
  per cases by A2,TARSKI:def 2;
  suppose
A3: x in ].PI/4,PI/2.[;
    then
A4: ex s be Real st s=x & PI/4 < s & s < PI/2;
A5: ex s be Real st s=x & PI/4 < s & s < PI/2 by A3;
A6: ].PI/4,PI/2.[ c= [.PI/4,PI/2.] by XXREAL_1:25;
    PI/4 in ].0,PI/2.] & PI/2 in ].0,PI/2.] by A1;
    then
A7: [.PI/4,PI/2.] c= ].0,PI/2.] by XXREAL_2:def 12;
    then
A8: cosec|[.PI/4,PI/2.] is decreasing by Th20,RFUNCT_2:29;
A9: [.PI/4,PI/2.] /\ dom cosec = [.PI/4,PI/2.] by A7,Th4,XBOOLE_1:1,28;
    then PI/2 in [.PI/4,PI/2.] /\ dom cosec by A1;
    then
A10: cosec.x > 1 by A3,A8,A9,A6,A5,Th32,RFUNCT_2:21;
    PI/4 in [.PI/4,PI/2.] by A1;
    then sqrt 2 > cosec.x by A3,A8,A9,A6,A4,Th32,RFUNCT_2:21;
    hence thesis by A10;
  end;
  suppose
    x = PI/4;
    hence thesis by Th32,SQUARE_1:19;
  end;
  suppose
    x = PI/2;
    hence thesis by Th32,SQUARE_1:19;
  end;
end;

Lm29: dom (sec | [.0,PI/4.]) = [.0,PI/4.]
proof
  [.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
  hence thesis by Th1,RELAT_1:62,XBOOLE_1:1;
end;

Lm30: dom (sec | [.3/4*PI,PI.]) = [.3/4*PI,PI.]
proof
  [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
  hence thesis by Th2,RELAT_1:62,XBOOLE_1:1;
end;

Lm31: dom (cosec | [.-PI/2,-PI/4.]) = [.-PI/2,-PI/4.]
proof
  [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
  hence thesis by Th3,RELAT_1:62,XBOOLE_1:1;
end;

Lm32: dom (cosec | [.PI/4,PI/2.]) = [.PI/4,PI/2.]
proof
  [.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
  hence thesis by Th4,RELAT_1:62,XBOOLE_1:1;
end;

Lm33: dom (sec|[.0,PI/2.[) = [.0,PI/2.[ & for th st th in [.0,PI/2.[ holds (
sec|[.0,PI/2.[).th = sec.th
proof
  dom (sec|[.0,PI/2.[) = dom sec /\ [.0,PI/2.[ by RELAT_1:61;
  then dom (sec|[.0,PI/2.[) = [.0,PI/2.[ by Th1,XBOOLE_1:28;
  hence thesis by FUNCT_1:47;
end;

Lm34: dom (sec|].PI/2,PI.]) = ].PI/2,PI.] & for th st th in ].PI/2,PI.] holds
(sec|].PI/2,PI.]).th = sec.th
proof
  dom (sec|].PI/2,PI.]) = dom sec /\ ].PI/2,PI.] by RELAT_1:61;
  then dom (sec|].PI/2,PI.]) = ].PI/2,PI.] by Th2,XBOOLE_1:28;
  hence thesis by FUNCT_1:47;
end;

Lm35: dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ & for th st th in [.-PI/2,0.[
holds (cosec|[.-PI/2,0.[).th = cosec.th
proof
  dom (cosec|[.-PI/2,0.[) = dom cosec /\ [.-PI/2,0.[ by RELAT_1:61;
  then dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ by Th3,XBOOLE_1:28;
  hence thesis by FUNCT_1:47;
end;

Lm36: dom (cosec|].0,PI/2.]) = ].0,PI/2.] & for th st th in ].0,PI/2.] holds (
cosec|].0,PI/2.]).th = cosec.th
proof
  dom (cosec|].0,PI/2.]) = dom cosec /\ ].0,PI/2.] by RELAT_1:61;
  then dom (cosec|].0,PI/2.]) = ].0,PI/2.] by Th4,XBOOLE_1:28;
  hence thesis by FUNCT_1:47;
end;

theorem Th37:
  sec|[.0,PI/2.[ is continuous
proof
  for th be real number st th in dom(sec|[.0,PI/2.[) holds sec|[.0,PI/2.[
  is_continuous_in th
  proof
    let th be real number;
A1: cos is_differentiable_in th by SIN_COS:63;
    assume
A2: th in dom(sec|[.0,PI/2.[);
    then th in [.0,PI/2.[ by RELAT_1:57;
    then cos.th <> 0 by Lm1,COMPTRIG:11;
    then
A3: sec is_continuous_in th by A1,FCONT_1:10,FDIFF_1:24;
    now
      let rseq;
      assume that
A4:   rng rseq c= dom (sec|[.0,PI/2.[) and
A5:   rseq is convergent & lim rseq = th;
A6:   dom (sec|[.0,PI/2.[) = [.0,PI/2.[ by Th1,RELAT_1:62;
      now
        let n be Element of NAT;
        dom (rseq) = NAT by SEQ_1:1;
        then rseq.n in rng rseq by FUNCT_1:def 3;
        then
A7:     (sec|[.0,PI/2.[).(rseq.n) = sec.(rseq.n) by A4,A6,FUNCT_1:49;
        (sec|[.0,PI/2.[).(rseq.n) = ((sec|[.0,PI/2.[)/*rseq).n by A4,
FUNCT_2:108;
        hence ((sec|[.0,PI/2.[)/*rseq).n = (sec/*rseq).n by A4,A6,A7,Th1,
FUNCT_2:108,XBOOLE_1:1;
      end;
      then
A8:   (sec|[.0,PI/2.[)/*rseq = sec/*rseq by FUNCT_2:63;
A9:   rng rseq c= dom sec by A4,A6,Th1,XBOOLE_1:1;
      then sec.th = lim(sec/*rseq) by A3,A5,FCONT_1:def 1;
      hence (sec|[.0,PI/2.[)/*rseq is convergent & (sec|[.0,PI/2.[).th = lim((
      sec|[.0,PI/2.[)/*rseq) by A2,A3,A5,A9,A8,Lm33,FCONT_1:def 1;
    end;
    hence thesis by FCONT_1:def 1;
  end;
  hence thesis by FCONT_1:def 2;
end;

theorem Th38:
  sec|].PI/2,PI.] is continuous
proof
  for th be real number st th in dom(sec|].PI/2,PI.]) holds sec|].PI/2,PI
  .] is_continuous_in th
  proof
    let th be real number;
A1: cos is_differentiable_in th by SIN_COS:63;
    assume
A2: th in dom(sec|].PI/2,PI.]);
    then th in ].PI/2,PI.] by RELAT_1:57;
    then cos.th <> 0 by Lm2,COMPTRIG:13;
    then
A3: sec is_continuous_in th by A1,FCONT_1:10,FDIFF_1:24;
    now
      let rseq;
      assume that
A4:   rng rseq c= dom (sec|].PI/2,PI.]) and
A5:   rseq is convergent & lim rseq = th;
A6:   dom (sec|].PI/2,PI.]) = ].PI/2,PI.] by Th2,RELAT_1:62;
      now
        let n be Element of NAT;
        dom (rseq) = NAT by SEQ_1:1;
        then rseq.n in rng rseq by FUNCT_1:def 3;
        then
A7:     (sec|].PI/2,PI.]).(rseq.n) = sec.(rseq.n) by A4,A6,FUNCT_1:49;
        (sec|].PI/2,PI.]).(rseq.n) = ((sec|].PI/2,PI.])/*rseq).n by A4,
FUNCT_2:108;
        hence ((sec|].PI/2,PI.])/*rseq).n = (sec/*rseq).n by A4,A6,A7,Th2,
FUNCT_2:108,XBOOLE_1:1;
      end;
      then
A8:   (sec|].PI/2,PI.])/*rseq = sec/*rseq by FUNCT_2:63;
A9:   rng rseq c= dom sec by A4,A6,Th2,XBOOLE_1:1;
      then sec.th = lim(sec/*rseq) by A3,A5,FCONT_1:def 1;
      hence
      (sec|].PI/2,PI.])/*rseq is convergent & (sec|].PI/2,PI.]).th = lim(
      (sec|].PI/2,PI.])/*rseq) by A2,A3,A5,A9,A8,Lm34,FCONT_1:def 1;
    end;
    hence thesis by FCONT_1:def 1;
  end;
  hence thesis by FCONT_1:def 2;
end;

theorem Th39:
  cosec|[.-PI/2,0.[ is continuous
proof
  for th be real number st th in dom(cosec|[.-PI/2,0.[) holds cosec|[.-PI/
  2,0.[ is_continuous_in th
  proof
    let th be real number;
    assume
A1: th in dom(cosec|[.-PI/2,0.[);
    then
A2: th in [.-PI/2,0.[ by RELAT_1:57;
    then th < 0 by Lm3,XXREAL_1:4;
    then
A3: th+2*PI < 0+2*PI by XREAL_1:8;
    -PI < th by A2,Lm3,XXREAL_1:4;
    then -PI+2*PI < th+2*PI by XREAL_1:8;
    then th+2*PI in ].PI,2*PI.[ by A3;
    then sin.(th+2*PI) <> 0 by COMPTRIG:9;
    then
A4: sin.th <> 0 by SIN_COS:78;
    sin is_differentiable_in th by SIN_COS:64;
    then
A5: cosec is_continuous_in th by A4,FCONT_1:10,FDIFF_1:24;
    now
      let rseq;
      assume that
A6:   rng rseq c= dom (cosec|[.-PI/2,0.[) and
A7:   rseq is convergent & lim rseq = th;
A8:   dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ by Th3,RELAT_1:62;
      now
        let n be Element of NAT;
        dom (rseq) = NAT by SEQ_1:1;
        then rseq.n in rng rseq by FUNCT_1:def 3;
        then
A9:     (cosec|[.-PI/2,0.[).(rseq.n) = cosec.(rseq.n) by A6,A8,FUNCT_1:49;
        (cosec|[.-PI/2,0.[).(rseq.n) = ((cosec|[.-PI/2,0.[)/*rseq).n by A6,
FUNCT_2:108;
        hence ((cosec|[.-PI/2,0.[)/*rseq).n = (cosec/*rseq).n by A6,A8,A9,Th3,
FUNCT_2:108,XBOOLE_1:1;
      end;
      then
A10:  (cosec|[.-PI/2,0.[)/*rseq = cosec/*rseq by FUNCT_2:63;
A11:  rng rseq c= dom cosec by A6,A8,Th3,XBOOLE_1:1;
      then cosec.th = lim(cosec/*rseq) by A5,A7,FCONT_1:def 1;
      hence (cosec|[.-PI/2,0.[)/*rseq is convergent & (cosec|[.-PI/2,0.[).th =
      lim((cosec|[.-PI/2,0.[)/*rseq) by A1,A5,A7,A11,A10,Lm35,FCONT_1:def 1;
    end;
    hence thesis by FCONT_1:def 1;
  end;
  hence thesis by FCONT_1:def 2;
end;

theorem Th40:
  cosec|].0,PI/2.] is continuous
proof
  for th be real number st th in dom(cosec|].0,PI/2.])holds cosec|].0,PI/2
  .] is_continuous_in th
  proof
    let th be real number;
A1: sin is_differentiable_in th by SIN_COS:64;
    assume
A2: th in dom(cosec|].0,PI/2.]);
    then th in ].0,PI/2.] by RELAT_1:57;
    then sin.th <> 0 by Lm4,COMPTRIG:7;
    then
A3: cosec is_continuous_in th by A1,FCONT_1:10,FDIFF_1:24;
    now
      let rseq;
      assume that
A4:   rng rseq c= dom (cosec|].0,PI/2.]) and
A5:   rseq is convergent & lim rseq = th;
A6:   dom (cosec|].0,PI/2.]) = ].0,PI/2.] by Th4,RELAT_1:62;
      now
        let n be Element of NAT;
        dom (rseq) = NAT by SEQ_1:1;
        then rseq.n in rng rseq by FUNCT_1:def 3;
        then
A7:     (cosec|].0,PI/2.]).(rseq.n) = cosec.(rseq.n) by A4,A6,FUNCT_1:49;
        (cosec|].0,PI/2.]).(rseq.n) = ((cosec|].0,PI/2.])/*rseq).n by A4,
FUNCT_2:108;
        hence ((cosec|].0,PI/2.])/*rseq).n = (cosec/*rseq).n by A4,A6,A7,Th4,
FUNCT_2:108,XBOOLE_1:1;
      end;
      then
A8:   (cosec|].0,PI/2.])/*rseq = cosec/*rseq by FUNCT_2:63;
A9:   rng rseq c= dom cosec by A4,A6,Th4,XBOOLE_1:1;
      then cosec.th = lim(cosec/*rseq) by A3,A5,FCONT_1:def 1;
      hence (cosec|].0,PI/2.])/*rseq is convergent & (cosec|].0,PI/2.]).th =
      lim((cosec|].0,PI/2.])/*rseq) by A2,A3,A5,A9,A8,Lm36,FCONT_1:def 1;
    end;
    hence thesis by FCONT_1:def 1;
  end;
  hence thesis by FCONT_1:def 2;
end;

theorem Th41:
  rng(sec | [.0,PI/4.]) = [.1,sqrt 2.]
proof
  now
    let y be set;
    thus y in [.1,sqrt 2.] implies ex x be set st x in dom (sec | [.0,PI/4.])
    & y = (sec | [.0,PI/4.]).x
    proof
      assume
A1:   y in [.1,sqrt 2.];
      then reconsider y1=y as Real;
      [.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
      then
A2:   sec|[.0,PI/4.] is continuous by Th37,FCONT_1:16;
      y1 in [.sec.0,sec.(PI/4).] \/ [.sec.(PI/4),sec.0.] by A1,Th31,
XBOOLE_0:def 3;
      then consider x be Real such that
A3:   x in [.0,PI/4.] & y1 = sec.x by A2,Lm13,Th1,FCONT_2:15,XBOOLE_1:1;
      take x;
      thus thesis by A3,Lm29,FUNCT_1:49;
    end;
    thus (ex x be set st x in dom (sec | [.0,PI/4.]) & y = (sec | [.0,PI/4.]).
    x) implies y in [.1,sqrt 2.]
    proof
      given x be set such that
A4:   x in dom (sec | [.0,PI/4.]) and
A5:   y = (sec | [.0,PI/4.]).x;
      reconsider x1=x as Real by A4;
      y = sec.x1 by A4,A5,Lm29,FUNCT_1:49;
      hence thesis by A4,Lm29,Th33;
    end;
  end;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th42:
  rng(sec | [.3/4*PI,PI.]) = [.-sqrt 2,-1.]
proof
  now
    let y be set;
    thus y in [.-sqrt 2,-1.] implies ex x be set st x in dom (sec | [.3/4*PI,
    PI.]) & y = (sec | [.3/4*PI,PI.]).x
    proof
      [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
      then
A1:   sec|[.3/4*PI,PI.] is continuous by Th38,FCONT_1:16;
      assume
A2:   y in [.-sqrt 2,-1.];
      then reconsider y1=y as Real;
A3:   3/4*PI <= PI by Lm6,XXREAL_1:2;
      y1 in [.sec.(3/4*PI),sec.PI.] \/ [.sec.PI,sec.(3/4*PI).] by A2,Th31,
XBOOLE_0:def 3;
      then consider x be Real such that
A4:   x in [.3/4*PI,PI.] & y1 = sec.x by A3,A1,Lm14,Th2,FCONT_2:15,XBOOLE_1:1;
      take x;
      thus thesis by A4,Lm30,FUNCT_1:49;
    end;
    thus (ex x be set st x in dom (sec | [.3/4*PI,PI.]) & y = (sec | [.3/4*PI,
    PI.]).x) implies y in [.-sqrt 2,-1.]
    proof
      given x be set such that
A5:   x in dom (sec | [.3/4*PI,PI.]) and
A6:   y = (sec | [.3/4*PI,PI.]).x;
      reconsider x1=x as Real by A5;
      y = sec.x1 by A5,A6,Lm30,FUNCT_1:49;
      hence thesis by A5,Lm30,Th34;
    end;
  end;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th43:
  rng(cosec | [.-PI/2,-PI/4.]) = [.-sqrt 2,-1.]
proof
  now
    let y be set;
    thus y in [.-sqrt 2,-1.] implies ex x be set st x in dom (cosec | [.-PI/2,
    -PI/4.]) & y = (cosec | [.-PI/2,-PI/4.]).x
    proof
      [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
      then
A1:   cosec|[.-PI/2,-PI/4.] is continuous by Th39,FCONT_1:16;
      assume
A2:   y in [.-sqrt 2,-1.];
      then reconsider y1=y as Real;
A3:   -PI/2 <= -PI/4 by Lm7,XXREAL_1:3;
      y1 in [.cosec.(-PI/4),cosec.(-PI/2).] \/ [.cosec.(-PI/2),cosec.(-PI/
      4).] by A2,Th32,XBOOLE_0:def 3;
      then consider x be Real such that
A4:   x in [.-PI/2,-PI/4.] & y1 = cosec.x by A3,A1,Lm19,Th3,FCONT_2:15
,XBOOLE_1:1;
      take x;
      thus thesis by A4,Lm31,FUNCT_1:49;
    end;
    thus (ex x be set st x in dom (cosec | [.-PI/2,-PI/4.]) & y = (cosec | [.-
    PI/2,-PI/4.]).x) implies y in [.-sqrt 2,-1.]
    proof
      given x be set such that
A5:   x in dom (cosec | [.-PI/2,-PI/4.]) and
A6:   y = (cosec | [.-PI/2,-PI/4.]).x;
      reconsider x1=x as Real by A5;
      y = cosec.x1 by A5,A6,Lm31,FUNCT_1:49;
      hence thesis by A5,Lm31,Th35;
    end;
  end;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th44:
  rng(cosec | [.PI/4,PI/2.]) = [.1,sqrt 2.]
proof
  now
    let y be set;
    thus y in [.1,sqrt 2.] implies ex x be set st x in dom (cosec | [.PI/4,PI/
    2.]) & y = (cosec | [.PI/4,PI/2.]).x
    proof
      [.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
      then
A1:   cosec|[.PI/4,PI/2.] is continuous by Th40,FCONT_1:16;
      assume
A2:   y in [.1,sqrt 2.];
      then reconsider y1=y as Real;
A3:   PI/4 <= PI/2 by Lm8,XXREAL_1:2;
      y1 in [.cosec.(PI/2),cosec.(PI/4).] \/ [.cosec.(PI/4),cosec.(PI/2).]
      by A2,Th32,XBOOLE_0:def 3;
      then consider x be Real such that
A4:   x in [.PI/4,PI/2.] & y1 = cosec.x by A3,A1,Lm20,Th4,FCONT_2:15,XBOOLE_1:1
;
      take x;
      thus thesis by A4,Lm32,FUNCT_1:49;
    end;
    thus (ex x be set st x in dom (cosec | [.PI/4,PI/2.]) & y = (cosec | [.PI/
    4,PI/2.]).x) implies y in [.1,sqrt 2.]
    proof
      given x be set such that
A5:   x in dom (cosec | [.PI/4,PI/2.]) and
A6:   y = (cosec | [.PI/4,PI/2.]).x;
      reconsider x1=x as Real by A5;
      y = cosec.x1 by A5,A6,Lm32,FUNCT_1:49;
      hence thesis by A5,Lm32,Th36;
    end;
  end;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th45:
  [.1,sqrt 2.] c= dom arcsec1
proof
A1: [.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
  rng(sec | [.0,PI/4.]) c= rng(sec | [.0,PI/2.[)
  proof
    let y be set;
    assume y in rng(sec | [.0,PI/4.]);
    then y in sec.:[.0,PI/4.] by RELAT_1:115;
    then ex x be set st x in dom sec & x in [.0,PI/4.] & y = sec .x by
FUNCT_1:def 6;
    then y in sec.:[.0,PI/2.[ by A1,FUNCT_1:def 6;
    hence thesis by RELAT_1:115;
  end;
  hence thesis by Th41,FUNCT_1:33;
end;

theorem Th46:
  [.-sqrt 2,-1.] c= dom arcsec2
proof
A1: [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
  rng(sec | [.3/4*PI,PI.]) c= rng(sec | ].PI/2,PI.])
  proof
    let y be set;
    assume y in rng(sec | [.3/4*PI,PI.]);
    then y in sec.:[.3/4*PI,PI.] by RELAT_1:115;
    then ex x be set st x in dom sec & x in [.3/4*PI,PI.] & y = sec.x by
FUNCT_1:def 6;
    then y in sec.:].PI/2,PI.] by A1,FUNCT_1:def 6;
    hence thesis by RELAT_1:115;
  end;
  hence thesis by Th42,FUNCT_1:33;
end;

theorem Th47:
  [.-sqrt 2,-1.] c= dom arccosec1
proof
A1: [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
  rng(cosec | [.-PI/2,-PI/4.]) c= rng(cosec | [.-PI/2,0.[)
  proof
    let y be set;
    assume y in rng(cosec | [.-PI/2,-PI/4.]);
    then y in cosec.:[.-PI/2,-PI/4.] by RELAT_1:115;
    then ex x be set st x in dom cosec & x in [.-PI/2,-PI/4.] & y = cosec.x by
FUNCT_1:def 6;
    then y in cosec.:[.-PI/2,0.[ by A1,FUNCT_1:def 6;
    hence thesis by RELAT_1:115;
  end;
  hence thesis by Th43,FUNCT_1:33;
end;

theorem Th48:
  [.1,sqrt 2.] c= dom arccosec2
proof
A1: [.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
  rng(cosec | [.PI/4,PI/2.]) c= rng(cosec | ].0,PI/2.])
  proof
    let y be set;
    assume y in rng(cosec | [.PI/4,PI/2.]);
    then y in cosec.:[.PI/4,PI/2.] by RELAT_1:115;
    then ex x be set st x in dom cosec & x in [.PI/4,PI/2.] & y = cosec.x by
FUNCT_1:def 6;
    then y in cosec.:].0,PI/2.] by A1,FUNCT_1:def 6;
    hence thesis by RELAT_1:115;
  end;
  hence thesis by Th44,FUNCT_1:33;
end;

Lm37: sec | [.0,PI/4.]|[.0,PI/4.] is increasing
proof
  [.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
  then sec|[.0,PI/4.] is increasing by Th17,RFUNCT_2:28;
  hence thesis;
end;

Lm38: sec | [.3/4*PI,PI.]|[.3/4*PI,PI.] is increasing
proof
  [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
  then sec|[.3/4*PI,PI.] is increasing by Th18,RFUNCT_2:28;
  hence thesis;
end;

Lm39: cosec | [.-PI/2,-PI/4.] |[.-PI/2,-PI/4.] is decreasing
proof
  [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
  then cosec|[.-PI/2,-PI/4.] is decreasing by Th19,RFUNCT_2:29;
  hence thesis;
end;

Lm40: cosec | [.PI/4,PI/2.]|[.PI/4,PI/2.] is decreasing
proof
  [.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
  then cosec|[.PI/4,PI/2.] is decreasing by Th20,RFUNCT_2:29;
  hence thesis;
end;

Lm41: sec | [.0,PI/4.] is one-to-one
proof
  [.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
  then (sec | [.0,PI/2.[) | [.0,PI/4.] = sec | [.0,PI/4.] by RELAT_1:74;
  hence thesis;
end;

Lm42: sec | [.3/4*PI,PI.] is one-to-one
proof
  [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
  then (sec | ].PI/2,PI.]) | [.3/4*PI,PI.] = sec | [.3/4*PI,PI.] by RELAT_1:74
;
  hence thesis;
end;

Lm43: cosec | [.-PI/2,-PI/4.] is one-to-one
proof
  [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
  then (cosec | [.-PI/2,0.[) | [.-PI/2,-PI/4.] = cosec | [.-PI/2,-PI/4.] by
RELAT_1:74;
  hence thesis;
end;

Lm44: cosec | [.PI/4,PI/2.] is one-to-one
proof
  [.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
  then (cosec | ].0,PI/2.]) | [.PI/4,PI/2.] = cosec | [.PI/4,PI/2.] by
RELAT_1:74;
  hence thesis;
end;

registration
  cluster sec | [.0,PI/4.] -> one-to-one;
  coherence by Lm41;
  cluster sec | [.3/4*PI,PI.] -> one-to-one;
  coherence by Lm42;
  cluster cosec | [.-PI/2,-PI/4.] -> one-to-one;
  coherence by Lm43;
  cluster cosec | [.PI/4,PI/2.] -> one-to-one;
  coherence by Lm44;
end;

theorem Th49:
  arcsec1 | [.1,sqrt 2.] = (sec | [.0,PI/4.])"
proof
  set h = sec | [.0,PI/2.[;
A1: [.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
  then (sec | [.0,PI/4.])" = (h | [.0,PI/4.])" by RELAT_1:74
    .= h" | (h.:[.0,PI/4.]) by RFUNCT_2:17
    .= h" | rng (h | [.0,PI/4.]) by RELAT_1:115
    .= h" | ([.1,sqrt 2.]) by A1,Th41,RELAT_1:74;
  hence thesis;
end;

theorem Th50:
  arcsec2 | [.-sqrt 2,-1.] = (sec | [.3/4*PI,PI.])"
proof
  set h = sec | ].PI/2,PI.];
A1: [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
  then (sec | [.3/4*PI,PI.])" = (h | [.3/4*PI,PI.])" by RELAT_1:74
    .= h" | (h.:[.3/4*PI,PI.]) by RFUNCT_2:17
    .= h" | rng (h | [.3/4*PI,PI.]) by RELAT_1:115
    .= h" | ([.-sqrt 2,-1.]) by A1,Th42,RELAT_1:74;
  hence thesis;
end;

theorem Th51:
  arccosec1 | [.-sqrt 2,-1.] = (cosec | [.-PI/2,-PI/4.])"
proof
  set h = cosec | [.-PI/2,0.[;
A1: [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
  then (cosec | [.-PI/2,-PI/4.])" = (h | [.-PI/2,-PI/4.])" by RELAT_1:74
    .= h" | (h.:[.-PI/2,-PI/4.]) by RFUNCT_2:17
    .= h" | rng (h | [.-PI/2,-PI/4.]) by RELAT_1:115
    .= h" | ([.-sqrt 2,-1.]) by A1,Th43,RELAT_1:74;
  hence thesis;
end;

theorem Th52:
  arccosec2 | [.1,sqrt 2.] = (cosec | [.PI/4,PI/2.])"
proof
  set h = cosec | ].0,PI/2.];
A1: [.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
  then (cosec | [.PI/4,PI/2.])" = (h | [.PI/4,PI/2.])" by RELAT_1:74
    .= h" | (h.:[.PI/4,PI/2.]) by RFUNCT_2:17
    .= h" | rng (h | [.PI/4,PI/2.]) by RELAT_1:115
    .= h" | ([.1,sqrt 2.]) by A1,Th44,RELAT_1:74;
  hence thesis;
end;

theorem
  (sec | [.0,PI/4.]) qua Function * (arcsec1 | [.1,sqrt 2.]) = id [.1,
  sqrt 2.] by Th41,Th49,FUNCT_1:39;

theorem
  (sec | [.3/4*PI,PI.]) qua Function * (arcsec2 | [.-sqrt 2,-1.]) = id
  [.-sqrt 2,-1.] by Th42,Th50,FUNCT_1:39;

theorem
  (cosec | [.-PI/2,-PI/4.]) qua Function * (arccosec1 | [.-sqrt 2,-1.])
  = id [.-sqrt 2,-1.] by Th43,Th51,FUNCT_1:39;

theorem
  (cosec | [.PI/4,PI/2.]) qua Function * (arccosec2 | [.1,sqrt 2.]) = id
  [.1,sqrt 2.] by Th44,Th52,FUNCT_1:39;

theorem
  (sec | [.0,PI/4.]) * (arcsec1 | [.1,sqrt 2.]) = id [.1,sqrt 2.] by Th41,Th49,
FUNCT_1:39;

theorem
  (sec | [.3/4*PI,PI.]) * (arcsec2 | [.-sqrt 2,-1.]) = id [.-sqrt 2,-1.]
  by Th42,Th50,FUNCT_1:39;

theorem
  (cosec | [.-PI/2,-PI/4.]) * (arccosec1 | [.-sqrt 2,-1.]) = id [.-sqrt
  2,-1.] by Th43,Th51,FUNCT_1:39;

theorem
  (cosec | [.PI/4,PI/2.]) * (arccosec2 | [.1,sqrt 2.]) = id [.1,sqrt 2.]
  by Th44,Th52,FUNCT_1:39;

theorem
  arcsec1 qua Function * (sec | [.0,PI/2.[) = id [.0,PI/2.[ by Lm25,Th25,
FUNCT_1:39;

theorem
  arcsec2 qua Function * (sec | ].PI/2,PI.]) = id ].PI/2,PI.] by Lm26,Th26,
FUNCT_1:39;

theorem
  arccosec1 qua Function * (cosec | [.-PI/2,0.[) = id [.-PI/2,0.[ by Lm27,Th27,
FUNCT_1:39;

theorem
  arccosec2 qua Function * (cosec | ].0,PI/2.]) = id ].0,PI/2.] by Lm28,Th28,
FUNCT_1:39;

theorem Th65:
  arcsec1 * (sec | [.0,PI/2.[) = id [.0,PI/2.[ by Lm25,Th25,FUNCT_1:39;

theorem Th66:
  arcsec2 * (sec | ].PI/2,PI.]) = id ].PI/2,PI.] by Lm26,Th26,FUNCT_1:39;

theorem Th67:
  arccosec1 * (cosec | [.-PI/2,0.[) = id [.-PI/2,0.[ by Lm27,Th27,FUNCT_1:39;

theorem Th68:
  arccosec2 * (cosec | ].0,PI/2.]) = id ].0,PI/2.] by Lm28,Th28,FUNCT_1:39;

theorem Th69:
  0 <= r & r < PI/2 implies arcsec1 sec.r = r
proof
A1: dom (sec | [.0,PI/2.[) = [.0,PI/2.[ by Th1,RELAT_1:62;
  assume 0 <= r & r < PI/2;
  then
A2: r in [.0,PI/2.[;
  then arcsec1 sec.r = arcsec1.((sec|[.0,PI/2.[).r) by FUNCT_1:49
    .= (id [.0,PI/2.[).r by A2,A1,Th65,FUNCT_1:13
    .= r by A2,FUNCT_1:18;
  hence thesis;
end;

theorem Th70:
  PI/2 < r & r <= PI implies arcsec2 sec.r = r
proof
A1: dom (sec | ].PI/2,PI.]) = ].PI/2,PI.] by Th2,RELAT_1:62;
  assume PI/2 < r & r <= PI;
  then
A2: r in ].PI/2,PI.];
  then arcsec2 sec.r = arcsec2.((sec|].PI/2,PI.]).r) by FUNCT_1:49
    .= (id ].PI/2,PI.]).r by A2,A1,Th66,FUNCT_1:13
    .= r by A2,FUNCT_1:18;
  hence thesis;
end;

theorem Th71:
  -PI/2 <= r & r < 0 implies arccosec1 cosec.r = r
proof
A1: dom (cosec | [.-PI/2,0.[) = [.-PI/2,0.[ by Th3,RELAT_1:62;
  assume -PI/2 <= r & r < 0;
  then
A2: r in [.-PI/2,0.[;
  then arccosec1 cosec.r = arccosec1.((cosec|[.-PI/2,0.[).r) by FUNCT_1:49
    .= (id [.-PI/2,0.[).r by A2,A1,Th67,FUNCT_1:13
    .= r by A2,FUNCT_1:18;
  hence thesis;
end;

theorem Th72:
  0 < r & r <= PI/2 implies arccosec2 cosec.r = r
proof
A1: dom (cosec | ].0,PI/2.]) = ].0,PI/2.] by Th4,RELAT_1:62;
  assume 0 < r & r <= PI/2;
  then
A2: r in ].0,PI/2.];
  then arccosec2 cosec.r = arccosec2.((cosec|].0,PI/2.]).r) by FUNCT_1:49
    .= (id ].0,PI/2.]).r by A2,A1,Th68,FUNCT_1:13
    .= r by A2,FUNCT_1:18;
  hence thesis;
end;

theorem Th73:
  arcsec1.1 = 0 & arcsec1.(sqrt 2) = PI/4
proof
A1: arcsec1.1 = arcsec1 1 .= 0 by Th31,Th69;
A2: PI/4 < PI/2 by Lm5,XXREAL_1:3;
  arcsec1.(sqrt 2) = arcsec1 (sqrt 2) .= PI/4 by A2,Th31,Th69;
  hence thesis by A1;
end;

theorem Th74:
  arcsec2.(-sqrt 2) = 3/4*PI & arcsec2.(-1) = PI
proof
A1: PI/2 < PI by Lm6,XXREAL_1:2;
A2: arcsec2.(-1) = arcsec2 (-1) .= PI by A1,Th31,Th70;
A3: PI/2 < 3/4*PI & 3/4*PI <= PI by Lm6,XXREAL_1:2;
  arcsec2.(-sqrt 2) = arcsec2 (-sqrt 2) .= 3/4*PI by A3,Th31,Th70;
  hence thesis by A2;
end;

theorem Th75:
  arccosec1.(-1) = -PI/2 & arccosec1.(-sqrt 2) = -PI/4
proof
A1: arccosec1.(-1) = arccosec1 (-1) .= -PI/2 by Th32,Th71;
A2: -PI/2 <= -PI/4 by Lm7,XXREAL_1:3;
  arccosec1.(-sqrt 2) = arccosec1 (-sqrt 2) .= -PI/4 by A2,Th32,Th71;
  hence thesis by A1;
end;

theorem Th76:
  arccosec2.(sqrt 2) = PI/4 & arccosec2.1 = PI/2
proof
A1: arccosec2.1 = arccosec2 1 .= PI/2 by Th32,Th72;
A2: PI/4 <= PI/2 by Lm8,XXREAL_1:2;
  arccosec2.(sqrt 2) = arccosec2 (sqrt 2) .= PI/4 by A2,Th32,Th72;
  hence thesis by A1;
end;

theorem Th77:
  arcsec1|(sec.:[.0,PI/2.[) is increasing
proof
  set f = sec | [.0,PI/2.[;
A1: f.:[.0,PI/2.[ = rng(f|[.0,PI/2.[) by RELAT_1:115
    .= rng(sec|[.0,PI/2.[) by RELAT_1:73
    .= sec.:[.0,PI/2.[ by RELAT_1:115;
  f|[.0,PI/2.[ = f by RELAT_1:73;
  hence thesis by A1,Th17,FCONT_3:9;
end;

theorem Th78:
  arcsec2|(sec.:].PI/2,PI.]) is increasing
proof
  set f = sec | ].PI/2,PI.];
A1: f.:].PI/2,PI.] = rng(f|].PI/2,PI.]) by RELAT_1:115
    .= rng(sec|].PI/2,PI.]) by RELAT_1:73
    .= sec.:].PI/2,PI.] by RELAT_1:115;
  f|].PI/2,PI.] = f by RELAT_1:73;
  hence thesis by A1,Th18,FCONT_3:9;
end;

theorem Th79:
  arccosec1|(cosec.:[.-PI/2,0.[) is decreasing
proof
  set f = cosec | [.-PI/2,0.[;
A1: f.:[.-PI/2,0.[ = rng(f|[.-PI/2,0.[) by RELAT_1:115
    .= rng(cosec|[.-PI/2,0.[) by RELAT_1:73
    .= cosec.:[.-PI/2,0.[ by RELAT_1:115;
  f|[.-PI/2,0.[ = f by RELAT_1:73;
  hence thesis by A1,Th19,FCONT_3:10;
end;

theorem Th80:
  arccosec2|(cosec.:].0,PI/2.]) is decreasing
proof
  set f = cosec | ].0,PI/2.];
A1: f.:].0,PI/2.] = rng(f|].0,PI/2.]) by RELAT_1:115
    .= rng(cosec|].0,PI/2.]) by RELAT_1:73
    .= cosec.:].0,PI/2.] by RELAT_1:115;
  f|].0,PI/2.] = f by RELAT_1:73;
  hence thesis by A1,Th20,FCONT_3:10;
end;

theorem Th81:
  arcsec1|[.1,sqrt 2.] is increasing
proof
  [.1,sqrt 2.] = sec.:[.0,PI/4.] & [.0,PI/4.] c= [.0,PI/2.[ by Lm5,Th41,
RELAT_1:115,XXREAL_2:def 12;
  hence thesis by Th77,RELAT_1:123,RFUNCT_2:28;
end;

theorem Th82:
  arcsec2|[.-sqrt 2,-1.] is increasing
proof
  [.-sqrt 2,-1.] = sec.:[.3/4*PI,PI.] & [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6
,Th42,RELAT_1:115,XXREAL_2:def 12;
  hence thesis by Th78,RELAT_1:123,RFUNCT_2:28;
end;

theorem Th83:
  arccosec1|[.-sqrt 2,-1.] is decreasing
proof
  [.-sqrt 2,-1.] = cosec.:[.-PI/2,-PI/4.] & [.-PI/2,-PI/4.] c= [.-PI/2,0.[
  by Lm7,Th43,RELAT_1:115,XXREAL_2:def 12;
  hence thesis by Th79,RELAT_1:123,RFUNCT_2:29;
end;

theorem Th84:
  arccosec2|[.1,sqrt 2.] is decreasing
proof
  [.1,sqrt 2.] = cosec.:[.PI/4,PI/2.] & [.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,Th44
,RELAT_1:115,XXREAL_2:def 12;
  hence thesis by Th80,RELAT_1:123,RFUNCT_2:29;
end;

theorem Th85:
  for x be set st x in [.1,sqrt 2.] holds arcsec1.x in [.0,PI/4.]
proof
  let x be set;
  assume x in [.1,sqrt 2.];
  then x in ].1,sqrt 2.[ \/ {1,sqrt 2} by SQUARE_1:19,XXREAL_1:128;
  then
A1: x in ].1,sqrt 2.[ or x in {1,sqrt 2} by XBOOLE_0:def 3;
  per cases by A1,TARSKI:def 2;
  suppose
A2: x in ].1,sqrt 2.[;
    then
A3: ].1,sqrt 2.[ c= [.1,sqrt 2.] & ex s be Real st s=x & 1 < s & s < sqrt
    2 by XXREAL_1:25;
A4: [.1,sqrt 2.] /\ dom arcsec1 = [.1,sqrt 2.] by Th45,XBOOLE_1:28;
    then sqrt 2 in [.1,sqrt 2.] /\ dom arcsec1 by SQUARE_1:19;
    then
A5: arcsec1.x < PI/4 by A2,A4,A3,Th73,Th81,RFUNCT_2:20;
    1 in [.1,sqrt 2.] by SQUARE_1:19;
    then 0 < arcsec1.x by A2,A4,A3,Th73,Th81,RFUNCT_2:20;
    hence thesis by A5;
  end;
  suppose
    x = 1;
    hence thesis by Th73;
  end;
  suppose
    x = sqrt 2;
    hence thesis by Th73;
  end;
end;

theorem Th86:
  for x be set st x in [.-sqrt 2,-1.] holds arcsec2.x in [.3/4*PI, PI.]
proof
  let x be set;
A1: -sqrt 2 < -1 by SQUARE_1:19,XREAL_1:24;
  assume x in [.-sqrt 2,-1.];
  then x in ].-sqrt 2,-1.[ \/ {-sqrt 2,-1} by A1,XXREAL_1:128;
  then
A2: x in ].-sqrt 2,-1.[ or x in {-sqrt 2,-1} by XBOOLE_0:def 3;
  per cases by A2,TARSKI:def 2;
  suppose
A3: x in ].-sqrt 2,-1.[;
    then
A4: ].-sqrt 2,-1.[ c= [.-sqrt 2,-1.] & ex s be Real st s=x & -sqrt 2 < s &
    s < - 1 by XXREAL_1:25;
A5: [.-sqrt 2,-1.] /\ dom arcsec2 = [.-sqrt 2,-1.] by Th46,XBOOLE_1:28;
    then -1 in [.-sqrt 2,-1.] /\ dom arcsec2 by A1;
    then
A6: arcsec2.x < PI by A3,A5,A4,Th74,Th82,RFUNCT_2:20;
    -sqrt 2 in [.-sqrt 2,-1.] by A1;
    then 3/4*PI < arcsec2.x by A3,A5,A4,Th74,Th82,RFUNCT_2:20;
    hence thesis by A6;
  end;
  suppose
A7: x = -sqrt 2;
    3/4*PI <= PI by Lm6,XXREAL_1:2;
    hence thesis by A7,Th74;
  end;
  suppose
A8: x = -1;
    3/4*PI <= PI by Lm6,XXREAL_1:2;
    hence thesis by A8,Th74;
  end;
end;

theorem Th87:
  for x be set st x in [.-sqrt 2,-1.] holds arccosec1.x in [.-PI/2 ,-PI/4.]
proof
  let x be set;
A1: -sqrt 2 < -1 by SQUARE_1:19,XREAL_1:24;
  assume x in [.-sqrt 2,-1.];
  then x in ].-sqrt 2,-1.[ \/ {-sqrt 2,-1} by A1,XXREAL_1:128;
  then
A2: x in ].-sqrt 2,-1.[ or x in {-sqrt 2,-1} by XBOOLE_0:def 3;
  per cases by A2,TARSKI:def 2;
  suppose
A3: x in ].-sqrt 2,-1.[;
    then
A4: ].-sqrt 2,-1.[ c= [.-sqrt 2,-1.] & ex s be Real st s=x & -sqrt 2 < s &
    s < - 1 by XXREAL_1:25;
A5: [.-sqrt 2,-1.] /\ dom arccosec1 = [.-sqrt 2,-1.] by Th47,XBOOLE_1:28;
    then -1 in [.-sqrt 2,-1.] /\ dom arccosec1 by A1;
    then
A6: arccosec1.x > -PI/2 by A3,A5,A4,Th75,Th83,RFUNCT_2:21;
    -sqrt 2 in [.-sqrt 2,-1.] by A1;
    then -PI/4 > arccosec1.x by A3,A5,A4,Th75,Th83,RFUNCT_2:21;
    hence thesis by A6;
  end;
  suppose
A7: x = -sqrt 2;
    -PI/2 <= -PI/4 by Lm7,XXREAL_1:3;
    hence thesis by A7,Th75;
  end;
  suppose
A8: x = -1;
    -PI/2 <= -PI/4 by Lm7,XXREAL_1:3;
    hence thesis by A8,Th75;
  end;
end;

theorem Th88:
  for x be set st x in [.1,sqrt 2.] holds arccosec2.x in [.PI/4,PI /2.]
proof
  let x be set;
  assume x in [.1,sqrt 2.];
  then x in ].1,sqrt 2.[ \/ {1,sqrt 2} by SQUARE_1:19,XXREAL_1:128;
  then
A1: x in ].1,sqrt 2.[ or x in {1,sqrt 2} by XBOOLE_0:def 3;
  per cases by A1,TARSKI:def 2;
  suppose
A2: x in ].1,sqrt 2.[;
    then
A3: ].1,sqrt 2.[ c= [.1,sqrt 2.] & ex s be Real st s=x & 1 < s & s < sqrt
    2 by XXREAL_1:25;
A4: [.1,sqrt 2.] /\ dom arccosec2 = [.1,sqrt 2.] by Th48,XBOOLE_1:28;
    then sqrt 2 in [.1,sqrt 2.] /\ dom arccosec2 by SQUARE_1:19;
    then
A5: arccosec2.x > PI/4 by A2,A4,A3,Th76,Th84,RFUNCT_2:21;
    1 in [.1,sqrt 2.] by SQUARE_1:19;
    then PI/2 > arccosec2.x by A2,A4,A3,Th76,Th84,RFUNCT_2:21;
    hence thesis by A5;
  end;
  suppose
A6: x = 1;
    PI/4 <= PI/2 by Lm8,XXREAL_1:2;
    hence thesis by A6,Th76;
  end;
  suppose
A7: x = sqrt 2;
    PI/4 <= PI/2 by Lm8,XXREAL_1:2;
    hence thesis by A7,Th76;
  end;
end;

theorem Th89:
  1 <= r & r <= sqrt 2 implies sec.(arcsec1 r) = r
proof
  assume 1 <= r & r <= sqrt 2;
  then
A1: r in [.1,sqrt 2.];
  then
A2: r in dom (arcsec1|[.1,sqrt 2.]) by Th45,RELAT_1:62;
  sec.(arcsec1 r) = ((sec|[.0,PI/4.]) qua Function).(arcsec1.r) by A1,Th85,
FUNCT_1:49
    .= ((sec|[.0,PI/4.]) qua Function).((arcsec1|[.1,sqrt 2.]).r) by A1,
FUNCT_1:49
    .= ((sec|[.0,PI/4.]) qua Function * (arcsec1|[.1,sqrt 2.])).r by A2,
FUNCT_1:13
    .= (id [.1,sqrt 2.]).r by Th41,Th49,FUNCT_1:39
    .= r by A1,FUNCT_1:18;
  hence thesis;
end;

theorem Th90:
  -sqrt 2 <= r & r <= -1 implies sec.(arcsec2 r ) = r
proof
  assume -sqrt 2 <= r & r <= -1;
  then
A1: r in [.-sqrt 2,-1.];
  then
A2: r in dom (arcsec2|[.-sqrt 2,-1.]) by Th46,RELAT_1:62;
  sec.(arcsec2 r) = ((sec|[.3/4*PI,PI.]) qua Function).(arcsec2.r) by A1,Th86,
FUNCT_1:49
    .= ((sec|[.3/4*PI,PI.]) qua Function).((arcsec2|[.-sqrt 2,-1.]).r) by A1,
FUNCT_1:49
    .= ((sec|[.3/4*PI,PI.]) qua Function * (arcsec2|[.-sqrt 2,-1.])).r by A2,
FUNCT_1:13
    .= (id [.-sqrt 2,-1.]).r by Th42,Th50,FUNCT_1:39
    .= r by A1,FUNCT_1:18;
  hence thesis;
end;

theorem Th91:
  -sqrt 2 <= r & r <= -1 implies cosec.(arccosec1 r) = r
proof
  assume -sqrt 2 <= r & r <= -1;
  then
A1: r in [.-sqrt 2,-1.];
  then
A2: r in dom (arccosec1|[.-sqrt 2,-1.]) by Th47,RELAT_1:62;
  cosec.(arccosec1 r) = ((cosec|[.-PI/2,-PI/4.]) qua Function).(arccosec1.
  r) by A1,Th87,FUNCT_1:49
    .= ((cosec|[.-PI/2,-PI/4.]) qua Function).((arccosec1|[.-sqrt 2,-1.]).r)
  by A1,FUNCT_1:49
    .= ((cosec|[.-PI/2,-PI/4.]) qua Function * (arccosec1|[.-sqrt 2,-1.])).r
  by A2,FUNCT_1:13
    .= (id [.-sqrt 2,-1.]).r by Th43,Th51,FUNCT_1:39
    .= r by A1,FUNCT_1:18;
  hence thesis;
end;

theorem Th92:
  1 <= r & r <= sqrt 2 implies cosec.(arccosec2 r) = r
proof
  assume 1 <= r & r <= sqrt 2;
  then
A1: r in [.1,sqrt 2.];
  then
A2: r in dom (arccosec2|[.1,sqrt 2.]) by Th48,RELAT_1:62;
  cosec.(arccosec2 r) = ((cosec|[.PI/4,PI/2.]) qua Function).(arccosec2.r)
  by A1,Th88,FUNCT_1:49
    .= ((cosec|[.PI/4,PI/2.]) qua Function).((arccosec2|[.1,sqrt 2.]).r) by A1,
FUNCT_1:49
    .= ((cosec|[.PI/4,PI/2.]) qua Function * (arccosec2|[.1,sqrt 2.])).r by A2,
FUNCT_1:13
    .= (id [.1,sqrt 2.]).r by Th44,Th52,FUNCT_1:39
    .= r by A1,FUNCT_1:18;
  hence thesis;
end;

theorem Th93:
  arcsec1|[.1,sqrt 2.] is continuous
proof
  set f = sec | [.0,PI/4.];
  f|[.0,PI/4.] = f & (f|[.0,PI/4.])"|(f.:[.0,PI/4.]) is continuous by Lm29,Lm37
,FCONT_1:47,RELAT_1:72;
  then arcsec1|[.1,sqrt 2.]|[.1,sqrt 2.] is continuous by Th41,Th49,RELAT_1:115
;
  hence thesis by FCONT_1:15;
end;

theorem Th94:
  arcsec2|[.-sqrt 2,-1.] is continuous
proof
  set f = sec | [.3/4*PI,PI.];
  3/4*PI <= PI by Lm6,XXREAL_1:2;
  then f|[.3/4*PI,PI.] = f & (f|[.3/4*PI,PI.])"|(f.:[.3/4*PI,PI.]) is
  continuous by Lm30,Lm38,FCONT_1:47,RELAT_1:72;
  then arcsec2|[.-sqrt 2,-1.]|[.-sqrt 2,-1.] is continuous by Th42,Th50,
RELAT_1:115;
  hence thesis by FCONT_1:15;
end;

theorem Th95:
  arccosec1|[.-sqrt 2,-1.] is continuous
proof
  set f = cosec | [.-PI/2,-PI/4.];
  -PI/2 <= -PI/4 by Lm7,XXREAL_1:3;
  then f|[.-PI/2,-PI/4.] = f & (f|[.-PI/2,-PI/4.])"|(f.:[.-PI/2,-PI/4.]) is
  continuous by Lm31,Lm39,FCONT_1:47,RELAT_1:72;
  then arccosec1|[.-sqrt 2,-1.]|[.-sqrt 2,-1.] is continuous by Th43,Th51,
RELAT_1:115;
  hence thesis by FCONT_1:15;
end;

theorem Th96:
  arccosec2|[.1,sqrt 2.] is continuous
proof
  set f = cosec | [.PI/4,PI/2.];
  PI/4 <= PI/2 by Lm8,XXREAL_1:2;
  then f|[.PI/4,PI/2.] = f & (f|[.PI/4,PI/2.])"|(f.:[.PI/4,PI/2.]) is
  continuous by Lm32,Lm40,FCONT_1:47,RELAT_1:72;
  then arccosec2|[.1,sqrt 2.]|[.1,sqrt 2.] is continuous by Th44,Th52,
RELAT_1:115;
  hence thesis by FCONT_1:15;
end;

theorem Th97:
  rng(arcsec1 | [.1,sqrt 2.]) = [.0,PI/4.]
proof
  now
    let y be set;
    thus y in [.0,PI/4.] implies ex x be set st x in dom (arcsec1 | [.1,sqrt 2
    .]) & y = (arcsec1 | [.1,sqrt 2.]).x
    proof
      assume
A1:   y in [.0,PI/4.];
      then reconsider y1=y as Real;
      y1 in [.arcsec1.1,arcsec1.(sqrt 2).] \/ [.arcsec1.(sqrt 2),arcsec1.1
      .] by A1,Th73,XBOOLE_0:def 3;
      then consider x be Real such that
A2:   x in [.1,sqrt 2.] & y1 = arcsec1.x by Th45,Th93,FCONT_2:15,SQUARE_1:19;
      take x;
      thus thesis by A2,Th45,FUNCT_1:49,RELAT_1:62;
    end;
    thus (ex x be set st x in dom (arcsec1 | [.1,sqrt 2.]) & y = (arcsec1 | [.
    1,sqrt 2.]).x) implies y in [.0,PI/4.]
    proof
      given x be set such that
A3:   x in dom (arcsec1 | [.1,sqrt 2.]) and
A4:   y = (arcsec1 | [.1,sqrt 2.]).x;
A5:   dom (arcsec1 | [.1,sqrt 2.]) = [.1,sqrt 2.] by Th45,RELAT_1:62;
      then y = arcsec1.x by A3,A4,FUNCT_1:49;
      hence thesis by A3,A5,Th85;
    end;
  end;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th98:
  rng(arcsec2 | [.-sqrt 2,-1.]) = [.3/4*PI,PI.]
proof
  now
    let y be set;
    thus y in [.3/4*PI,PI.] implies ex x be set st x in dom (arcsec2 | [.-sqrt
    2,-1.]) & y = (arcsec2 | [.-sqrt 2,-1.]).x
    proof
      assume
A1:   y in [.3/4*PI,PI.];
      then reconsider y1=y as Real;
      -sqrt 2 < -1 & y1 in [.arcsec2.(-sqrt 2),arcsec2.(-1).] \/ [.arcsec2
.(-1), arcsec2.(-sqrt 2).] by A1,Th74,SQUARE_1:19,XBOOLE_0:def 3,XREAL_1:24;
      then consider x be Real such that
A2:   x in [.-sqrt 2,-1.] & y1 = arcsec2.x by Th46,Th94,FCONT_2:15;
      take x;
      thus thesis by A2,Th46,FUNCT_1:49,RELAT_1:62;
    end;
    thus (ex x be set st x in dom (arcsec2 | [.-sqrt 2,-1.]) & y = (arcsec2 |
    [.-sqrt 2,-1.]).x) implies y in [.3/4*PI,PI.]
    proof
      given x be set such that
A3:   x in dom (arcsec2 | [.-sqrt 2,-1.]) and
A4:   y = (arcsec2 | [.-sqrt 2,-1.]).x;
A5:   dom (arcsec2 | [.-sqrt 2,-1.]) = [.-sqrt 2,-1.] by Th46,RELAT_1:62;
      then y = arcsec2.x by A3,A4,FUNCT_1:49;
      hence thesis by A3,A5,Th86;
    end;
  end;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th99:
  rng(arccosec1 | [.-sqrt 2,-1.]) = [.-PI/2,-PI/4.]
proof
  now
    let y be set;
    thus y in [.-PI/2,-PI/4.] implies ex x be set st x in dom (arccosec1 | [.-
    sqrt 2,-1.]) & y = (arccosec1 | [.-sqrt 2,-1.]).x
    proof
      assume
A1:   y in [.-PI/2,-PI/4.];
      then reconsider y1=y as Real;
      -sqrt 2 < -1 & y1 in [.arccosec1.(-1),arccosec1.(-sqrt 2).] \/ [.
arccosec1.( -sqrt 2),arccosec1.(-1).] by A1,Th75,SQUARE_1:19,XBOOLE_0:def 3
,XREAL_1:24;
      then consider x be Real such that
A2:   x in [.-sqrt 2,-1.] & y1 = arccosec1.x by Th47,Th95,FCONT_2:15;
      take x;
      thus thesis by A2,Th47,FUNCT_1:49,RELAT_1:62;
    end;
    thus (ex x be set st x in dom (arccosec1 | [.-sqrt 2,-1.]) & y = (
    arccosec1 | [.-sqrt 2,-1.]).x) implies y in [.-PI/2,-PI/4.]
    proof
      given x be set such that
A3:   x in dom (arccosec1 | [.-sqrt 2,-1.]) and
A4:   y = (arccosec1 | [.-sqrt 2,-1.]).x;
A5:   dom (arccosec1 | [.-sqrt 2,-1.]) = [.-sqrt 2,-1.] by Th47,RELAT_1:62;
      then y = arccosec1.x by A3,A4,FUNCT_1:49;
      hence thesis by A3,A5,Th87;
    end;
  end;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th100:
  rng(arccosec2 | [.1,sqrt 2.]) = [.PI/4,PI/2.]
proof
  now
    let y be set;
    thus y in [.PI/4,PI/2.] implies ex x be set st x in dom (arccosec2 | [.1,
    sqrt 2.]) & y = (arccosec2 | [.1,sqrt 2.]).x
    proof
      assume
A1:   y in [.PI/4,PI/2.];
      then reconsider y1=y as Real;
      y1 in [.arccosec2.(sqrt 2),arccosec2.1.] \/ [.arccosec2.1,arccosec2.
      (sqrt 2).] by A1,Th76,XBOOLE_0:def 3;
      then consider x be Real such that
A2:   x in [.1,sqrt 2.] & y1 = arccosec2.x by Th48,Th96,FCONT_2:15,SQUARE_1:19;
      take x;
      thus thesis by A2,Th48,FUNCT_1:49,RELAT_1:62;
    end;
    thus (ex x be set st x in dom (arccosec2 | [.1,sqrt 2.]) & y = (arccosec2
    | [.1,sqrt 2.]).x) implies y in [.PI/4,PI/2.]
    proof
      given x be set such that
A3:   x in dom (arccosec2 | [.1,sqrt 2.]) and
A4:   y = (arccosec2 | [.1,sqrt 2.]).x;
A5:   dom (arccosec2 | [.1,sqrt 2.]) = [.1,sqrt 2.] by Th48,RELAT_1:62;
      then y = arccosec2.x by A3,A4,FUNCT_1:49;
      hence thesis by A3,A5,Th88;
    end;
  end;
  hence thesis by FUNCT_1:def 3;
end;

theorem
  (1 <= r & r <= sqrt 2 & arcsec1 r = 0 implies r = 1) & (1 <= r & r <=
  sqrt 2 & arcsec1 r = PI/4 implies r = sqrt 2) by Th31,Th89;

theorem
  (-sqrt 2 <= r & r <= -1 & arcsec2 r = 3/4*PI implies r = -sqrt 2) & (-
  sqrt 2 <= r & r <= -1 & arcsec2 r = PI implies r = -1) by Th31,Th90;

theorem
  (-sqrt 2 <= r & r <= -1 & arccosec1 r = -PI/2 implies r = -1) & (-sqrt
  2 <= r & r <= -1 & arccosec1 r = -PI/4 implies r = -sqrt 2) by Th32,Th91;

theorem
  (1 <= r & r <= sqrt 2 & arccosec2 r = PI/4 implies r = sqrt 2) & (1 <=
  r & r <= sqrt 2 & arccosec2 r = PI/2 implies r = 1) by Th32,Th92;

theorem Th105:
  1 <= r & r <= sqrt 2 implies 0 <= arcsec1 r & arcsec1 r <= PI/4
proof
  assume 1 <= r & r <= sqrt 2;
  then
A1: r in [.1,sqrt 2.];
  then r in dom (arcsec1 | [.1,sqrt 2.]) by Th45,RELAT_1:62;
  then (arcsec1 | [.1,sqrt 2.]).r in rng(arcsec1 | [.1,sqrt 2.]) by
FUNCT_1:def 3;
  then arcsec1 r in rng(arcsec1 | [.1,sqrt 2.]) by A1,FUNCT_1:49;
  hence thesis by Th97,XXREAL_1:1;
end;

theorem Th106:
  -sqrt 2 <= r & r <= -1 implies 3/4*PI <= arcsec2 r & arcsec2 r <= PI
proof
  assume -sqrt 2 <= r & r <= -1;
  then
A1: r in [.-sqrt 2,-1.];
  then r in dom (arcsec2 | [.-sqrt 2,-1.]) by Th46,RELAT_1:62;
  then (arcsec2 | [.-sqrt 2,-1.]).r in rng(arcsec2 | [.-sqrt 2,-1.]) by
FUNCT_1:def 3;
  then arcsec2 r in rng(arcsec2 | [.-sqrt 2,-1.]) by A1,FUNCT_1:49;
  hence thesis by Th98,XXREAL_1:1;
end;

theorem Th107:
  -sqrt 2 <= r & r <= -1 implies -PI/2 <= arccosec1 r & arccosec1 r <= -PI/4
proof
  assume -sqrt 2 <= r & r <= -1;
  then
A1: r in [.-sqrt 2,-1.];
  then r in dom (arccosec1 | [.-sqrt 2,-1.]) by Th47,RELAT_1:62;
  then (arccosec1 | [.-sqrt 2,-1.]).r in rng(arccosec1 | [.-sqrt 2,-1.]) by
FUNCT_1:def 3;
  then arccosec1 r in rng(arccosec1 | [.-sqrt 2,-1.]) by A1,FUNCT_1:49;
  hence thesis by Th99,XXREAL_1:1;
end;

theorem Th108:
  1 <= r & r <= sqrt 2 implies PI/4 <= arccosec2 r & arccosec2 r <= PI/2
proof
  assume 1 <= r & r <= sqrt 2;
  then
A1: r in [.1,sqrt 2.];
  then r in dom (arccosec2 | [.1,sqrt 2.]) by Th48,RELAT_1:62;
  then (arccosec2 | [.1,sqrt 2.]).r in rng(arccosec2 | [.1,sqrt 2.]) by
FUNCT_1:def 3;
  then arccosec2 r in rng(arccosec2 | [.1,sqrt 2.]) by A1,FUNCT_1:49;
  hence thesis by Th100,XXREAL_1:1;
end;

theorem Th109:
  1 < r & r < sqrt 2 implies 0 < arcsec1 r & arcsec1 r < PI/4
proof
  assume
A1: 1 < r & r < sqrt 2;
  then arcsec1 r <= PI/4 by Th105;
  then
  0 < arcsec1 r & arcsec1 r < PI/4 or 0 = arcsec1 r or arcsec1 r = PI/4 by A1
,Th105,XXREAL_0:1;
  hence thesis by A1,Th31,Th89;
end;

theorem Th110:
  -sqrt 2 < r & r < -1 implies 3/4*PI < arcsec2 r & arcsec2 r < PI
proof
  assume
A1: -sqrt 2 < r & r < -1;
  then 3/4*PI <= arcsec2 r & arcsec2 r <= PI by Th106;
  then
  3/4*PI < arcsec2 r & arcsec2 r < PI or 3/4*PI = arcsec2 r or arcsec2 r =
  PI by XXREAL_0:1;
  hence thesis by A1,Th31,Th90;
end;

theorem Th111:
  -sqrt 2 < r & r < -1 implies -PI/2 < arccosec1 r & arccosec1 r < -PI/4
proof
  assume
A1: -sqrt 2 < r & r < -1;
  then -PI/2 <= arccosec1 r & arccosec1 r <= -PI/4 by Th107;
  then -PI/2 < arccosec1 r & arccosec1 r < -PI/4 or -PI/2 = arccosec1 r or
  arccosec1 r = -PI/4 by XXREAL_0:1;
  hence thesis by A1,Th32,Th91;
end;

theorem Th112:
  1 < r & r < sqrt 2 implies PI/4 < arccosec2 r & arccosec2 r < PI/2
proof
  assume
A1: 1 < r & r < sqrt 2;
  then PI/4 <= arccosec2 r & arccosec2 r <= PI/2 by Th108;
  then PI/4 < arccosec2 r & arccosec2 r < PI/2 or PI/4 = arccosec2 r or
  arccosec2 r = PI/2 by XXREAL_0:1;
  hence thesis by A1,Th32,Th92;
end;

theorem Th113:
  1 <= r & r <= sqrt 2 implies sin.(arcsec1 r) = sqrt(r^2-1)/r &
  cos.(arcsec1 r) = 1/r
proof
  set x = arcsec1 r;
  assume that
A1: 1 <= r and
A2: r <= sqrt 2;
  r in [.1,sqrt 2.] by A1,A2;
  then
A3: x in dom (sec | [.0,PI/4.]) by Lm29,Th85;
  PI/4 < PI/1 by XREAL_1:76;
  then 0 in [.0,PI.] & PI/4 in [.0,PI.];
  then [.0,PI/4.] c= [.0,PI.] by XXREAL_2:def 12;
  then
A4: sin.x >= 0 by A3,Lm29,COMPTRIG:8;
A5: dom (sec | [.0,PI/4.]) c= dom sec by RELAT_1:60;
A6: r = (cos^).x by A1,A2,Th89
    .= 1/cos.x by A3,A5,RFUNCT_1:def 2;
  r^2 >= 1^2 by A1,SQUARE_1:15;
  then
A7: r^2-1 >= 0 by XREAL_1:48;
  (sin.x)^2+(cos.x)^2 = 1 by SIN_COS:28;
  then (sin.x)^2 = 1-(cos.x)^2 .= 1-(1/r)*(1/r) by A6
    .= 1-1/(r^2) by XCMPLX_1:102
    .= (r^2)/(r^2)-1/(r^2) by A1,XCMPLX_1:60
    .= (r^2-1)/(r^2);
  then sin.x = sqrt ((r^2-1)/(r^2)) by A4,SQUARE_1:def 2
    .= sqrt(r^2-1)/sqrt(r^2) by A1,A7,SQUARE_1:30
    .= sqrt(r^2-1)/r by A1,SQUARE_1:22;
  hence thesis by A6;
end;

theorem Th114:
  -sqrt 2 <= r & r <= -1 implies sin.(arcsec2 r) = -sqrt(r^2-1)/r
  & cos.(arcsec2 r) = 1/r
proof
  3/4*PI <= PI by Lm6,XXREAL_1:2;
  then
A1: 3/4*PI in [.0,PI.];
A2: dom (sec | [.3/4*PI,PI.]) c= dom sec by RELAT_1:60;
  set x = arcsec2 r;
  assume that
A3: -sqrt 2 <= r and
A4: r <= -1;
  r in [.-sqrt 2,-1.] by A3,A4;
  then
A5: x in dom (sec | [.3/4*PI,PI.]) by Lm30,Th86;
A6: r = (cos^).x by A3,A4,Th90
    .= 1/cos.x by A5,A2,RFUNCT_1:def 2;
  PI in [.0,PI.];
  then [.3/4*PI,PI.] c= [.0,PI.] by A1,XXREAL_2:def 12;
  then
A7: sin.x >= 0 by A5,Lm30,COMPTRIG:8;
  -r >= -(-1) by A4,XREAL_1:24;
  then (-r)^2 >= 1^2 by SQUARE_1:15;
  then
A8: r^2-1 >= 0 by XREAL_1:48;
  (sin.x)^2+(cos.x)^2 = 1 by SIN_COS:28;
  then (sin.x)^2 = 1-(cos.x)^2 .= 1-(1/r)*(1/r) by A6
    .= 1-1/(r^2) by XCMPLX_1:102
    .= (r^2)/(r^2)-1/(r^2) by A4,XCMPLX_1:60
    .= (r^2-1)/(r^2);
  then sin.x = sqrt ((r^2-1)/(r^2)) by A7,SQUARE_1:def 2
    .= sqrt(r^2-1)/sqrt(r^2) by A4,A8,SQUARE_1:30
    .= sqrt(r^2-1)/(-r) by A4,SQUARE_1:23
    .= -sqrt(r^2-1)/r by XCMPLX_1:188;
  hence thesis by A6;
end;

theorem Th115:
  -sqrt 2 <= r & r <= -1 implies sin.(arccosec1 r) = 1/r & cos.(
  arccosec1 r) = -sqrt(r^2-1)/r
proof
  set x = arccosec1 r;
  assume that
A1: -sqrt 2 <= r and
A2: r <= -1;
  r in [.-sqrt 2,-1.] by A1,A2;
  then
A3: x in dom (cosec | [.-PI/2,-PI/4.]) by Lm31,Th87;
  -PI/4 >= -PI/2 by Lm7,XXREAL_1:3;
  then -PI/2 in [.-PI/2,PI/2.] & -PI/4 in [.-PI/2,PI/2.];
  then [.-PI/2,-PI/4.] c= [.-PI/2,PI/2.] by XXREAL_2:def 12;
  then
A4: cos.x >= 0 by A3,Lm31,COMPTRIG:12;
A5: dom (cosec | [.-PI/2,-PI/4.]) c= dom cosec by RELAT_1:60;
A6: r = (sin^).x by A1,A2,Th91
    .= 1/sin.x by A3,A5,RFUNCT_1:def 2;
  -r >= -(-1) by A2,XREAL_1:24;
  then (-r)^2 >= 1^2 by SQUARE_1:15;
  then
A7: r^2-1 >= 0 by XREAL_1:48;
  (sin.x)^2+(cos.x)^2 = 1 by SIN_COS:28;
  then (cos.x)^2 = 1-(sin.x)^2 .= 1-(1/r)*(1/r) by A6
    .= 1-1/(r^2) by XCMPLX_1:102
    .= (r^2)/(r^2)-1/(r^2) by A2,XCMPLX_1:60
    .= (r^2-1)/(r^2);
  then cos.x = sqrt ((r^2-1)/(r^2)) by A4,SQUARE_1:def 2
    .= sqrt(r^2-1)/sqrt(r^2) by A2,A7,SQUARE_1:30
    .= sqrt(r^2-1)/(-r) by A2,SQUARE_1:23
    .= -sqrt(r^2-1)/r by XCMPLX_1:188;
  hence thesis by A6;
end;

theorem Th116:
  1 <= r & r <= sqrt 2 implies sin.(arccosec2 r) = 1/r & cos.(
  arccosec2 r) = sqrt(r^2-1)/r
proof
  PI/4 <= PI/2 by Lm8,XXREAL_1:2;
  then
A1: PI/4 in [.-PI/2,PI/2.];
A2: dom (cosec | [.PI/4,PI/2.]) c= dom cosec by RELAT_1:60;
  set x = arccosec2 r;
  assume that
A3: 1 <= r and
A4: r <= sqrt 2;
  r in [.1,sqrt 2.] by A3,A4;
  then
A5: x in dom (cosec | [.PI/4,PI/2.]) by Lm32,Th88;
A6: r = (sin^).x by A3,A4,Th92
    .= 1/sin.x by A5,A2,RFUNCT_1:def 2;
  PI/2 in [.-PI/2,PI/2.];
  then [.PI/4,PI/2.] c= [.-PI/2,PI/2.] by A1,XXREAL_2:def 12;
  then
A7: cos.x >= 0 by A5,Lm32,COMPTRIG:12;
  r^2 >= 1^2 by A3,SQUARE_1:15;
  then
A8: r^2-1 >= 0 by XREAL_1:48;
  (sin.x)^2+(cos.x)^2 = 1 by SIN_COS:28;
  then (cos.x)^2 = 1-(sin.x)^2 .= 1-(1/r)*(1/r) by A6
    .= 1-1/(r^2) by XCMPLX_1:102
    .= (r^2)/(r^2)-1/(r^2) by A3,XCMPLX_1:60
    .= (r^2-1)/(r^2);
  then cos.x = sqrt ((r^2-1)/(r^2)) by A7,SQUARE_1:def 2
    .= sqrt(r^2-1)/sqrt(r^2) by A3,A8,SQUARE_1:30
    .= sqrt(r^2-1)/r by A3,SQUARE_1:22;
  hence thesis by A6;
end;

theorem
  1 < r & r < sqrt 2 implies cosec.(arcsec1 r) = r/sqrt(r^2-1)
proof
  set x = arcsec1 r;
  ].0,PI/2.] = ].0,PI/2.[ \/ {PI/2} by XXREAL_1:132;
  then
A1: ].0,PI/2.[ c= ].0,PI/2.] by XBOOLE_1:7;
  PI/4 < PI/2 by XREAL_1:76;
  then ].0,PI/4.[ c= ].0,PI/2.[ by XXREAL_1:46;
  then ].0,PI/4.[ c= ].0,PI/2.] by A1,XBOOLE_1:1;
  then
A2: ].0,PI/4.[ c= dom cosec by Th4,XBOOLE_1:1;
  assume
A3: 1 < r & r < sqrt 2;
  then 0 < arcsec1 r & arcsec1 r < PI/4 by Th109;
  then x in ].0,PI/4.[;
  then cosec.x = 1/sin.x by A2,RFUNCT_1:def 2
    .= 1/(sqrt(r^2-1)/r) by A3,Th113
    .= r/sqrt(r^2-1) by XCMPLX_1:57;
  hence thesis;
end;

theorem
  -sqrt 2 < r & r < -1 implies cosec.(arcsec2 r) = -r/sqrt(r^2-1)
proof
  set x = arcsec2 r;
A1: ].3/4*PI,PI.[ c= dom cosec
  proof
    ].3/4*PI,PI.[ /\ sin"{0} = {}
    proof
      assume ].3/4*PI,PI.[ /\ sin"{0} <> {};
      then consider rr such that
A2:   rr in ].3/4*PI,PI.[ /\ sin"{0} by XBOOLE_0:def 1;
      rr in sin"{0} by A2,XBOOLE_0:def 4;
      then
A3:   sin.rr in {0} by FUNCT_1:def 7;
A4:   ].3/4*PI,PI.[ c= ].0,PI.[ by XXREAL_1:46;
      rr in ].3/4*PI,PI.[ by A2,XBOOLE_0:def 4;
      then sin.rr <> 0 by A4,COMPTRIG:7;
      hence contradiction by A3,TARSKI:def 1;
    end;
    then ].3/4*PI,PI.[ \ sin"{0} c= dom sin \ sin"{0} & ].3/4*PI,PI.[ misses
    sin"{0} by SIN_COS:24,XBOOLE_0:def 7,XBOOLE_1:33;
    then ].3/4*PI,PI.[ c= dom sin \ sin"{0} by XBOOLE_1:83;
    hence thesis by RFUNCT_1:def 2;
  end;
  assume
A5: -sqrt 2 < r & r < -1;
  then 3/4*PI < arcsec2 r & arcsec2 r < PI by Th110;
  then x in ].3/4*PI,PI.[;
  then cosec.x = 1/sin.x by A1,RFUNCT_1:def 2
    .= 1/(-sqrt(r^2-1)/r) by A5,Th114
    .= -1/(sqrt(r^2-1)/r) by XCMPLX_1:188
    .= -r/sqrt(r^2-1) by XCMPLX_1:57;
  hence thesis;
end;

theorem
  -sqrt 2 < r & r < -1 implies sec.(arccosec1 r) = -r/sqrt(r^2-1)
proof
  set x = arccosec1 r;
A1: ].-PI/2,-PI/4.[ c= dom sec
  proof
    ].-PI/2,-PI/4.[ /\ cos"{0} = {}
    proof
      assume ].-PI/2,-PI/4.[ /\ cos"{0} <> {};
      then consider rr such that
A2:   rr in ].-PI/2,-PI/4.[ /\ cos"{0} by XBOOLE_0:def 1;
      rr in cos"{0} by A2,XBOOLE_0:def 4;
      then
A3:   cos.rr in {0} by FUNCT_1:def 7;
A4:   ].-PI/2,-PI/4.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
      rr in ].-PI/2,-PI/4.[ by A2,XBOOLE_0:def 4;
      then cos.rr <> 0 by A4,COMPTRIG:11;
      hence contradiction by A3,TARSKI:def 1;
    end;
    then ].-PI/2,-PI/4.[ \ cos"{0} c= dom cos \ cos"{0} & ].-PI/2,-PI/4.[
    misses cos" {0} by SIN_COS:24,XBOOLE_0:def 7,XBOOLE_1:33;
    then ].-PI/2,-PI/4.[ c= dom cos \ cos"{0} by XBOOLE_1:83;
    hence thesis by RFUNCT_1:def 2;
  end;
  assume
A5: -sqrt 2 < r & r < -1;
  then -PI/2 < arccosec1 r & arccosec1 r < -PI/4 by Th111;
  then x in ].-PI/2,-PI/4.[;
  then sec.x = 1/cos.x by A1,RFUNCT_1:def 2
    .= 1/(-sqrt(r^2-1)/r) by A5,Th115
    .= -1/(sqrt(r^2-1)/r) by XCMPLX_1:188
    .= -r/sqrt(r^2-1) by XCMPLX_1:57;
  hence thesis;
end;

theorem
  1 < r & r < sqrt 2 implies sec.(arccosec2 r) = r/sqrt(r^2-1)
proof
  set x = arccosec2 r;
  [.0,PI/2.[ = ].0,PI/2.[ \/ {0} by XXREAL_1:131;
  then ].PI/4,PI/2.[ c= ].0,PI/2.[ & ].0,PI/2.[ c= [.0,PI/2.[ by XBOOLE_1:7
,XXREAL_1:46;
  then ].PI/4,PI/2.[ c= [.0,PI/2.[ by XBOOLE_1:1;
  then
A1: ].PI/4,PI/2.[ c= dom sec by Th1,XBOOLE_1:1;
  assume
A2: 1 < r & r < sqrt 2;
  then PI/4 < arccosec2 r & arccosec2 r < PI/2 by Th112;
  then x in ].PI/4,PI/2.[;
  then sec.x = 1/cos.x by A1,RFUNCT_1:def 2
    .= 1/(sqrt(r^2-1)/r) by A2,Th116
    .= r/sqrt(r^2-1) by XCMPLX_1:57;
  hence thesis;
end;

theorem Th121:
  arcsec1 is_differentiable_on sec.:].0,PI/2.[
proof
  set X = sec.:].0,PI/2.[;
  set g1 = arcsec1|(sec.:].0,PI/2.[);
  set f = sec|[.0,PI/2.[;
  set g = f|].0,PI/2.[;
A1: g = sec|].0,PI/2.[ by RELAT_1:74,XXREAL_1:22;
A2: dom ((g|].0,PI/2.[)") = rng (g|].0,PI/2.[) by FUNCT_1:33
    .= rng(sec|].0,PI/2.[) by A1,RELAT_1:72
    .= sec.:].0,PI/2.[ by RELAT_1:115;
A3: (g|].0,PI/2.[)" = (f|].0,PI/2.[)" by RELAT_1:72
    .= arcsec1|(f.:].0,PI/2.[) by RFUNCT_2:17
    .= arcsec1|(rng(f|].0,PI/2.[)) by RELAT_1:115
    .= arcsec1|(rng (sec|].0,PI/2.[)) by RELAT_1:74,XXREAL_1:22
    .= arcsec1|(sec.:].0,PI/2.[) by RELAT_1:115;
A4: g is_differentiable_on ].0,PI/2.[ by A1,Th5,FDIFF_2:16;
  now
A5: for x0 be Real st x0 in ].0,PI/2.[ holds sin.x0/(cos.x0)^2 > 0
    proof
      let x0 be Real;
      assume
A6:   x0 in ].0,PI/2.[;
      ].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
      then
A7:   cos.x0 > 0 by A6,COMPTRIG:11;
      ].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:5,XXREAL_1:46;
      then sin.x0 > 0 by A6,COMPTRIG:7;
      hence thesis by A7;
    end;
    let x0 be Real such that
A8: x0 in ].0,PI/2.[;
    diff(g,x0) = (g`|].0,PI/2.[).x0 by A4,A8,FDIFF_1:def 7
      .= ((sec|].0,PI/2.[)`|].0,PI/2.[).x0 by RELAT_1:74,XXREAL_1:22
      .= (sec`|].0,PI/2.[).x0 by Th5,FDIFF_2:16
      .= diff(sec,x0) by A8,Th5,FDIFF_1:def 7
      .= sin.x0/(cos.x0)^2 by A8,Th5;
    hence diff(g,x0) > 0 by A8,A5;
  end;
  then
A9: g1 is_differentiable_on X by A2,A4,A3,Lm21,FDIFF_2:48;
A10: for x st x in X holds arcsec1|X is_differentiable_in x
  proof
    let x;
    assume x in X;
    then g1|X is_differentiable_in x by A9,FDIFF_1:def 6;
    hence thesis by RELAT_1:72;
  end;
  X c= dom arcsec1 by A2,A3,RELAT_1:60;
  hence thesis by A10,FDIFF_1:def 6;
end;

theorem Th122:
  arcsec2 is_differentiable_on sec.:].PI/2,PI.[
proof
  set X = sec.:].PI/2,PI.[;
  set g1 = arcsec2|(sec.:].PI/2,PI.[);
  set f = sec|].PI/2,PI.];
  set g = f|].PI/2,PI.[;
A1: g = sec|].PI/2,PI.[ by RELAT_1:74,XXREAL_1:21;
A2: dom ((g|].PI/2,PI.[)") = rng (g|].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: (g|].PI/2,PI.[)" = (f|].PI/2,PI.[)" by RELAT_1:72
    .= arcsec2|(f.:].PI/2,PI.[) by RFUNCT_2:17
    .= arcsec2|(rng(f|].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: g is_differentiable_on ].PI/2,PI.[ by A1,Th6,FDIFF_2:16;
  now
A5: for x0 be Real st x0 in ].PI/2,PI.[ holds sin.x0/(cos.x0)^2 > 0
    proof
      let x0 be Real;
      assume
A6:   x0 in ].PI/2,PI.[;
      ].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 thesis by A7;
    end;
    let x0 be Real such that
A8: x0 in ].PI/2,PI.[;
    diff(g,x0) = (g`|].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(g,x0) > 0 by A8,A5;
  end;
  then
A9: g1 is_differentiable_on X by A2,A4,A3,Lm22,FDIFF_2:48;
A10: for x st x in X holds arcsec2|X is_differentiable_in x
  proof
    let x;
    assume x in X;
    then g1|X is_differentiable_in x by A9,FDIFF_1:def 6;
    hence thesis by RELAT_1:72;
  end;
  X c= dom arcsec2 by A2,A3,RELAT_1:60;
  hence thesis by A10,FDIFF_1:def 6;
end;

theorem Th123:
  arccosec1 is_differentiable_on cosec.:].-PI/2,0.[
proof
  set X = cosec.:].-PI/2,0.[;
  set g1 = arccosec1|(cosec.:].-PI/2,0.[);
  set f = cosec|[.-PI/2,0.[;
  set g = f|].-PI/2,0.[;
A1: g = cosec|].-PI/2,0.[ by RELAT_1:74,XXREAL_1:22;
A2: dom ((g|].-PI/2,0.[)") = rng (g|].-PI/2,0.[) by FUNCT_1:33
    .= rng(cosec|].-PI/2,0.[) by A1,RELAT_1:72
    .= cosec.:].-PI/2,0.[ by RELAT_1:115;
A3: (g|].-PI/2,0.[)" = (f|].-PI/2,0.[)" by RELAT_1:72
    .= arccosec1|(f.:].-PI/2,0.[) by RFUNCT_2:17
    .= arccosec1|(rng(f|].-PI/2,0.[)) by RELAT_1:115
    .= arccosec1|(rng (cosec|].-PI/2,0.[)) by RELAT_1:74,XXREAL_1:22
    .= arccosec1|(cosec.:].-PI/2,0.[) by RELAT_1:115;
A4: g is_differentiable_on ].-PI/2,0.[ by A1,Th7,FDIFF_2:16;
  now
A5: for x0 be Real st x0 in ].-PI/2,0.[ holds -cos.x0/(sin.x0)^2 < 0
    proof
      let x0 be Real;
      assume
A6:   x0 in ].-PI/2,0.[;
      then x0 < 0 by XXREAL_1:4;
      then
A7:   x0+2*PI < 0+2*PI by XREAL_1:8;
      ].-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 by A6,XXREAL_1:4;
      then -PI+2*PI < x0+2*PI by XREAL_1:8;
      then x0+2*PI in ].PI,2*PI.[ by A7;
      then sin.(x0+2*PI) < 0 by COMPTRIG:9;
      then
A8:   sin.x0 < 0 by SIN_COS:78;
      ].-PI/2,0.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
      then cos.x0 > 0 by A6,COMPTRIG:11;
      hence thesis by A8;
    end;
    let x0 be Real such that
A9: x0 in ].-PI/2,0.[;
    diff(g,x0) = (g`|].-PI/2,0.[).x0 by A4,A9,FDIFF_1:def 7
      .= ((cosec|].-PI/2,0.[)`|].-PI/2,0.[).x0 by RELAT_1:74,XXREAL_1:22
      .= (cosec`|].-PI/2,0.[).x0 by Th7,FDIFF_2:16
      .= diff(cosec,x0) by A9,Th7,FDIFF_1:def 7
      .= -cos.x0/(sin.x0)^2 by A9,Th7;
    hence diff(g,x0) < 0 by A9,A5;
  end;
  then
A10: g1 is_differentiable_on X by A2,A4,A3,Lm23,FDIFF_2:48;
A11: for x st x in X holds arccosec1|X is_differentiable_in x
  proof
    let x;
    assume x in X;
    then g1|X is_differentiable_in x by A10,FDIFF_1:def 6;
    hence thesis by RELAT_1:72;
  end;
  X c= dom arccosec1 by A2,A3,RELAT_1:60;
  hence thesis by A11,FDIFF_1:def 6;
end;

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

theorem
  sec.:].0,PI/2.[ is open
proof
  for x0 be Real st x0 in ].0,PI/2.[ holds diff(sec,x0) > 0
  proof
    let x0 be Real;
    assume
A1: x0 in ].0,PI/2.[;
    ].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
    then
A2: cos.x0 > 0 by A1,COMPTRIG:11;
    ].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:5,XXREAL_1:46;
    then sin.x0 > 0 by A1,COMPTRIG:7;
    then sin.x0/(cos.x0)^2 > 0/(cos.x0)^2 by A2;
    hence thesis by A1,Th5;
  end;
  then rng(sec|].0,PI/2.[) is open by Lm10,Th5,FDIFF_2:41;
  hence thesis by RELAT_1:115;
end;

theorem
  sec.:].PI/2,PI.[ is open
proof
  for x0 be Real st x0 in ].PI/2,PI.[ holds diff(sec,x0) > 0
  proof
    let x0 be Real;
    assume
A1: x0 in ].PI/2,PI.[;
    ].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by COMPTRIG:5,XXREAL_1:46;
    then
A2: cos.x0 < 0 by A1,COMPTRIG:13;
    ].PI/2,PI.[ c= ].0,PI.[ by XXREAL_1:46;
    then sin.x0 > 0 by A1,COMPTRIG:7;
    then sin.x0/(cos.x0)^2 > 0/(cos.x0)^2 by A2;
    hence thesis by A1,Th6;
  end;
  then rng(sec|].PI/2,PI.[) is open by Lm12,Th6,FDIFF_2:41;
  hence thesis by RELAT_1:115;
end;

theorem
  cosec.:].-PI/2,0.[ is open
proof
  for x0 be Real st x0 in ].-PI/2,0.[ holds diff(cosec,x0) < 0
  proof
    let x0 be Real;
    assume
A1: x0 in ].-PI/2,0.[;
    then x0 < 0 by XXREAL_1:4;
    then
A2: x0+2*PI < 0+2*PI by XREAL_1:8;
    ].-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 by A1,XXREAL_1:4;
    then -PI+2*PI < x0+2*PI by XREAL_1:8;
    then x0+2*PI in ].PI,2*PI.[ by A2;
    then sin.(x0+2*PI) < 0 by COMPTRIG:9;
    then
A3: sin.x0 < 0 by SIN_COS:78;
    ].-PI/2,0.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
    then cos.x0 > 0 by A1,COMPTRIG:11;
    then -(cos.x0/(sin.x0)^2) < -0 by A3;
    hence thesis by A1,Th7;
  end;
  then rng(cosec|].-PI/2,0.[) is open by Lm16,Th7,FDIFF_2:41;
  hence thesis by RELAT_1:115;
end;

theorem
  cosec.:].0,PI/2.[ is open
proof
  for x0 be Real st x0 in ].0,PI/2.[ holds diff(cosec,x0) < 0
  proof
    let x0 be Real;
    assume
A1: x0 in ].0,PI/2.[;
    ].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
    then
A2: cos.x0 > 0 by A1,COMPTRIG:11;
    ].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:5,XXREAL_1:46;
    then sin.x0 > 0 by A1,COMPTRIG:7;
    then -(cos.x0/(sin.x0)^2) < -0 by A2;
    hence thesis by A1,Th8;
  end;
  then rng(cosec|].0,PI/2.[) is open by Lm18,Th8,FDIFF_2:41;
  hence thesis by RELAT_1:115;
end;

theorem
  arcsec1|(sec.:].0,PI/2.[) is continuous by Th121,FDIFF_1:25;

theorem
  arcsec2|(sec.:].PI/2,PI.[) is continuous by Th122,FDIFF_1:25;

theorem
  arccosec1|(cosec.:].-PI/2,0.[) is continuous by Th123,FDIFF_1:25;

theorem
  arccosec2|(cosec.:].0,PI/2.[) is continuous by Th124,FDIFF_1:25;