:: Inverse Trigonometric Functions Arcsec1, Arcsec2, Arccosec1 and Arccosec2
::  by Bing Xie , Xiquan Liang and Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008 Association of Mizar Users

environ

 vocabularies FUNCT_1, RELAT_1, PRE_TOPC, ARYTM_1, ARYTM_3, PARTFUN1, SIN_COS,
      FDIFF_1, SQUARE_1, FINSEQ_1, SIN_COS4, ORDINAL2, ARYTM, BOOLE, SEQ_1,
      RCOMP_1, INT_1, FCONT_1, RFUNCT_2, SINCOS10, SEQ_2;
 notations TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, FUNCT_1, RELSET_1, PARTFUN1,
      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,
      RCOMP_2, SEQ_2;
 constructors REAL_1, SQUARE_1, RCOMP_1, RFUNCT_1, FDIFF_1, RFUNCT_2, FCONT_1,
      SIN_COS, PARTFUN2, SIN_COS4, TOPALG_2, FDIFF_9, RCOMP_2, SEQ_1, SEQ_2;
 registrations XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RELSET_1,
      FUNCT_1, SIN_COS6, RFUNCT_2, ORDINAL1, INT_1, VALUED_0;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
 definitions TARSKI, FDIFF_9, XCMPLX_0, RCOMP_2, RFUNCT_2, SQUARE_1;
 theorems SIN_COS6, FDIFF_2, XCMPLX_1, FDIFF_1, RELAT_1, SIN_COS, COMPTRIG,
      RFUNCT_2, FCONT_1, FUNCT_1, RCOMP_1, REAL_1, XBOOLE_0, SQUARE_1, FCONT_3,
      XREAL_1, TARSKI, XBOOLE_1, ROLLE, RFUNCT_1, REAL_2, FCONT_2, SEQ_1,
      FDIFF_9, RCOMP_2, XXREAL_0, FUNCT_2, XXREAL_1;

begin ::  arcsec, arccosec

reserve x, r, s, h for Real,
        a, b, p, q, th for real number,
        i for integer number,
        n for Element of NAT,
        rr, y for set,
        Z for open Subset of REAL,
        X, Y for Subset of REAL,
        rseq for Real_Sequence,
        f, f1, f2, g for PartFunc of REAL,REAL;

Lm1:
 [.0,PI/2.[ c= ].-PI/2,PI/2.[
proof
    PI in ].0,4.[ by SIN_COS:def 32;then
    PI > 0 by XXREAL_1:4;then
A2: 0/2 < PI/2 by XREAL_1:76;
A3: 0 - PI/2 < 0 by XREAL_1:51;
A4: ].0,PI/2.[ c= ].-PI/2,PI/2.[ by A3,XXREAL_1:46;
    0 - PI < 0 by XREAL_1:51;
    then (-PI)/2 < 0/2 by XREAL_1:76;then
A5: 0 in ].-PI/2,PI/2.[ by A2,XXREAL_1:4;
    {0} c= ].-PI/2,PI/2.[
    proof
      let x be set;
      assume x in {0};
      hence x in ].-PI/2,PI/2.[ by A5,TARSKI:def 1;
    end;
    then ].0,PI/2.[ \/ {0} c= ].-PI/2,PI/2.[ by A4,XBOOLE_1:8;
    hence [.0,PI/2.[ c= ].-PI/2,PI/2.[ by A2,XXREAL_1:131;
end;

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

Lm2:
  ].PI/2,PI.] c= ].PI/2,3/2*PI.[
proof
    PI in ].0,4.[ by SIN_COS:def 32;then
A1: PI > 0 by XXREAL_1:4;then
A2: PI < 3/2*PI by REAL_2:144;
A3: ].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by A2,XXREAL_1:46;
A4: PI/2 < PI/1 by A1,REAL_2:200;then
A5: PI in ].PI/2,3/2*PI.[ by A2,XXREAL_1:4;
    {PI} c= ].PI/2,3/2*PI.[
    proof
      let x be set;
      assume x in {PI};
      hence x in ].PI/2,3/2*PI.[ by A5,TARSKI:def 1;
    end;
    then ].PI/2,PI.[ \/ {PI} c= ].PI/2,3/2*PI.[ by A3,XBOOLE_1:8;
    hence ].PI/2,PI.] c= ].PI/2,3/2*PI.[ by A4,XXREAL_1:132;
end;

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

Lm3:
  [.-PI/2,0.[ c= ].-PI,0.[
proof
    PI in ].0,4.[ by SIN_COS:def 32;then
    PI > 0 by XXREAL_1:4;
    then PI/2 < PI/1 by REAL_2:200;then
A2: -PI < -PI/2 by XREAL_1:26;then
A3: ].-PI/2,0.[ c= ].-PI,0.[ by XXREAL_1:46;
A4: -PI/2 < -0;then
A5: -PI/2 in ].-PI,0.[ by A2,XXREAL_1:4;
    {-PI/2} c= ].-PI,0.[
    proof
      let x be set;
      assume x in {-PI/2};
      hence x in ].-PI,0.[ by A5,TARSKI:def 1;
    end;
    then ].-PI/2,0.[ \/ {-PI/2} c= ].-PI,0.[ by A3,XBOOLE_1:8;
    hence [.-PI/2,0.[ c= ].-PI,0.[ by A4,XXREAL_1:131;
end;

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

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

theorem Th4:
  ].0,PI/2.] c= dom cosec
proof
    set f = sin^;
A1: ].0,PI/2.] \ sin"{0} c= dom sin \ sin"{0} by SIN_COS:27,XBOOLE_1:33;
    ].0,PI/2.] /\ sin"{0} = {}
    proof
        assume ].0,PI/2.] /\ sin"{0} <> {};
        then consider rr such that
    A2: rr in ].0,PI/2.] /\ sin"{0} by XBOOLE_0:def 1;
    A3: rr in ].0,PI/2.] & rr in sin"{0} by A2,XBOOLE_0:def 3;
    A5: sin.rr <> 0 by A3,Lm4,COMPTRIG:23;
        sin.rr in {0} by A3,FUNCT_1:def 13;
        hence contradiction by A5,TARSKI:def 1;
    end;
    then ].0,PI/2.] misses sin"{0} by XBOOLE_0:def 7;
    then ].0,PI/2.] c= dom sin \ sin"{0} by A1,XBOOLE_1:83;
    hence ].0,PI/2.] c= dom cosec by RFUNCT_1:def 8;
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.[;
    PI in ].0,4.[ by SIN_COS:def 32;
    then PI > 0 by XXREAL_1:4;
    then PI/2 > 0/2 by XREAL_1:76;
    then [.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;
        diff(sec,x) = ((sec)`|Z).x by A2,A3,FDIFF_1:def 8
        .= 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 in ].0,4.[ by SIN_COS:def 32;
    then PI > 0 by XXREAL_1:4;
    then PI/2 < PI/1 by REAL_2:200;
    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;
      diff(sec,x) = ((sec)`|Z).x by A2,A3,FDIFF_1:def 8
      .= 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;
    then [.-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;
      diff(cosec,x) = ((cosec)`|Z).x by A2,A3,FDIFF_1:def 8
      .= -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.[;
    PI in ].0,4.[ by SIN_COS:def 32;
    then PI > 0 by XXREAL_1:4;
    then PI/2 > 0/2 by XREAL_1:76;
    then ].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;
      diff(cosec,x) = ((cosec)`|Z).x by A2,A3,FDIFF_1:def 8
      .= -cos.x/(sin.x)^2 by A1,A3,FDIFF_9:5;
      hence thesis;
    end;
    hence thesis by A1,FDIFF_9:5;
end;

theorem
  sec is_continuous_on ].0,PI/2.[ by Th5,FDIFF_1:33;

theorem
  sec is_continuous_on ].PI/2,PI.[ by Th6,FDIFF_1:33;

theorem
  cosec is_continuous_on ].-PI/2,0.[ by Th7,FDIFF_1:33;

theorem
  cosec is_continuous_on ].0,PI/2.[ by Th8,FDIFF_1:33;

theorem Th13:
  sec is_increasing_on ].0,PI/2.[
proof
    PI in ].0,4.[ by SIN_COS:def 32;then
A1: PI > 0 by XXREAL_1:4;then
A2: PI/2 > 0/2 by XREAL_1:76;
    for x be Real st x in ].0,PI/2.[ holds diff(sec,x) > 0
    proof
      let x be Real;
      assume
  A4: x in ].0,PI/2.[;
      PI/2 < PI/1 by A1,REAL_2:200;
      then ].0,PI/2.[ c= ].0,PI.[ by XXREAL_1:46;then
  A5: sin.x > 0 by A4,COMPTRIG:23;
      0 - PI/2 < 0 by XREAL_1:51;
      then ].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
      then cos.x > 0 by A4,COMPTRIG:27;
      then (cos.x)^2 > 0 by SQUARE_1:74;
      then sin.x/(cos.x)^2 > 0/(cos.x)^2 by A5,REAL_1:73;
      hence thesis by A4,Th5;
    end;
    hence thesis by A2,Th5,ROLLE:9;
end;

theorem Th14:
  sec is_increasing_on ].PI/2,PI.[
proof
A0: PI in ].0,4.[ by SIN_COS:def 32;then
A1: PI > 0 by XXREAL_1:4;
A3: for x be Real st x in ].PI/2,PI.[ holds diff(sec,x) > 0
    proof
      let x be Real;
      assume
  A4: x in ].PI/2,PI.[;
      PI/2 > 0/2 by A1,XREAL_1:76;
      then ].PI/2,PI.[ c= ].0,PI.[ by XXREAL_1:46;then
  A5: sin.x > 0 by A4,COMPTRIG:23;
      PI > 0 by A0,XXREAL_1:4;
      then PI <= 3/2*PI by REAL_2:146;
      then ].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by XXREAL_1:46;
      then cos.x < 0 by A4,COMPTRIG:29;
      then (cos.x)^2 > 0 by SQUARE_1:74;
      then sin.x/(cos.x)^2 > 0/(cos.x)^2 by A5,REAL_1:73;
      hence thesis by A4,Th6;
    end;
    PI > 0 by A0,XXREAL_1:4;
    then PI/2 < PI/1 by REAL_2:200;
    hence thesis by A3,Th6,ROLLE:9;
end;

theorem Th15:
  cosec is_decreasing_on ].-PI/2,0.[
proof
    for x be Real st x in ].-PI/2,0.[ holds diff(cosec,x) < 0
    proof
      let x be Real;
      assume
  A2: x in ].-PI/2,0.[;
      ].-PI/2,0.[ \/ {-PI/2} = [.-PI/2,0.[ by COMPTRIG:21,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 & x < 0 by A2,XXREAL_1:4;
      then -PI+2*PI < x+2*PI & x+2*PI < 0+2*PI by XREAL_1:10;
      then x+2*PI in ].PI,2*PI.[ by XXREAL_1:4;
      then sin.(x+2*PI) < 0 by COMPTRIG:25;
      then sin.x < 0 by SIN_COS:83;then
  A3: (sin.x)^2 > 0 by SQUARE_1:74;
      ].-PI/2,0.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,XXREAL_1:46;
      then cos.x > 0 by A2,COMPTRIG:27;
      then cos.x/(sin.x)^2 > 0/(sin.x)^2 by A3,REAL_1:73;
      then -cos.x/(sin.x)^2 < -0 by XREAL_1:26;
      hence thesis by A2,Th7;
    end;
    hence thesis by Th7,COMPTRIG:21,ROLLE:10;
end;

theorem Th16:
  cosec is_decreasing_on ].0,PI/2.[
proof
    for x be Real st x in ].0,PI/2.[ holds diff(cosec,x) < 0
    proof
      let x be Real;
      assume
  A2: x in ].0,PI/2.[;
      ].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:21,XXREAL_1:46;
      then sin.x > 0 by A2,COMPTRIG:23;then
  A3: (sin.x)^2 > 0 by SQUARE_1:74;
      ].0,PI/2.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,XXREAL_1:46;
      then cos.x > 0 by A2,COMPTRIG:27;
      then cos.x/(sin.x)^2 > 0/(sin.x)^2 by A3,REAL_1:73;
      then -cos.x/(sin.x)^2 < -0 by XREAL_1:26;
      hence thesis by A2,Th8;
    end;
    hence thesis by Th8,COMPTRIG:21,ROLLE:10;
end;

theorem Th17:
  sec is_increasing_on [.0,PI/2.[
proof
    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 [.0,PI/2.[ & r1 in dom sec & r2 in [.0,PI/2.[ & r2 in dom sec
    by A1,A2,XBOOLE_0:def 3;then
A5: 0 <= r1 & r1 < PI/2 & 0 <= r2 & r2 < PI/2 by XXREAL_1:3;
    now per cases by A5,REAL_1:def 5;
      suppose
   A6:  0 = r1;
        PI in ].0,4.[ by SIN_COS:def 32;then
   A7:  PI > 0 by XXREAL_1:4;
   A8:  sec.r1 = 1/1 by A4,A6,RFUNCT_1:def 8,SIN_COS:33
        .= 1;
   A9:  -PI/2 < r2 & r2 < PI/2 by A4,Lm1,XXREAL_1:4;
        -PI/2+2*PI*0 < r2 & r2 < PI/2+2*PI*0 by A4,Lm1,XXREAL_1:4;then
        cos r2 > 0 by SIN_COS6:13;then
   A10: cos.r2 > 0 by SIN_COS:def 23;
        PI/2 < 2*PI by A7,XREAL_1:70;
        then r2 < 2*PI by A9,XXREAL_0:2;
        then cos r2 < 1 by A3,A6,SIN_COS6:34;
        then cos.r2 < 1 by SIN_COS:def 23;
        then 1/1 < 1/cos.r2 by A10,XREAL_1:78;
        hence sec.r2 > sec.r1 by A4,A8,RFUNCT_1:def 8;
      end;
      suppose
   A13: 0 < r1;
        then r1 in ].0,PI/2.[ by A5,XXREAL_1:4;then
   A14: r1 in ].0,PI/2.[ /\ dom sec by A4,XBOOLE_0:def 3;
        0 < r2 by A3,A13,XXREAL_0:2;
        then r2 in ].0,PI/2.[ by A5,XXREAL_1:4;
        then r2 in ].0,PI/2.[ /\ dom sec by A4,XBOOLE_0:def 3;
        hence sec.r2 > sec.r1 by A3,A14,Th13,RFUNCT_2:def 2;
      end;
    end;
    hence sec.r2 > sec.r1;
end;

theorem Th18:
  sec is_increasing_on ].PI/2,PI.]
proof
    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 ].PI/2,PI.] & r1 in dom sec & r2 in ].PI/2,PI.] & r2 in dom sec
    by A1,A2,XBOOLE_0:def 3;then
A5: PI/2 < r1 & r1 <= PI & PI/2 < r2 & r2 <= PI by XXREAL_1:2;
    now per cases by A5,REAL_1:def 5;
      suppose
      A6: r2 < PI;
          then r1 < PI by A3,XXREAL_0:2;
          then r1 in ].PI/2,PI.[ by A5,XXREAL_1:4;then
      A7: r1 in ].PI/2,PI.[ /\ dom sec by A4,XBOOLE_0:def 3;
          r2 in ].PI/2,PI.[ by A5,A6,XXREAL_1:4;
          then r2 in ].PI/2,PI.[ /\ dom sec by A4,XBOOLE_0:def 3;
          hence sec.r2 > sec.r1 by A3,A7,Th14,RFUNCT_2:def 2;
      end;
      suppose
      A8:  r2 = PI;
      A9:  sec.r2 = 1/(-1) by A4,A8,RFUNCT_1:def 8,SIN_COS:81
           .= -1;
           PI in ].0,4.[ by SIN_COS:def 32;then
      A10: PI > 0 by XXREAL_1:4;
           then PI*1 < PI*(3/2) by XREAL_1:70;
           then PI/2+2*PI*0 < r1 & r1 < 3/2*PI+2*PI*0
           by A3,A4,A8,XXREAL_1:2,XXREAL_0:2;
           then cos r1 < 0 by SIN_COS6:14;then
      A11: cos.r1 < 0 by SIN_COS:def 23;
           PI/2 > 0/2 by A10,XREAL_1:76;
           then r1 > 0 & r1 < PI by A3,A5,XXREAL_0:2;
           then cos r1 > -1 by SIN_COS6:35;
           then cos.r1 > -1 by SIN_COS:def 23;
           then (cos.r1)" < (-1)" by A11,XREAL_1:89;
           hence sec.r1 < sec.r2 by A4,A9,RFUNCT_1:def 8;
      end;
    end;
    hence sec.r2 > sec.r1;
end;

theorem Th19:
  cosec is_decreasing_on [.-PI/2,0.[
proof
    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 [.-PI/2,0.[ & r1 in dom cosec & r2 in [.-PI/2,0.[ & r2 in dom cosec
    by A1,A2,XBOOLE_0:def 3;then
A5: -PI/2 <= r1 & r1 < 0 & -PI/2 <= r2 & r2 < 0 by XXREAL_1:3;
    now per cases by A5,REAL_1:def 5;
      suppose
      A6: -PI/2 = r1;
      A7: cosec.r1 = 1/sin.(-PI/2) by A4,A6,RFUNCT_1:def 8
          .= 1/(-1) by SIN_COS:33,SIN_COS:81
          .= -1;
      A8: r2 in ].-PI/2,0.[ by A3,A5,A6,XXREAL_1:4;
          -PI/2 > -PI by COMPTRIG:21,XREAL_1:26;
          then ].-PI/2,0.[ c= ].-PI,0.[ by XXREAL_1:46;
          then -PI < r2 & r2 < 0 by A8,XXREAL_1:4;
          then -PI+2*PI < r2+2*PI & r2+2*PI < 0+2*PI by XREAL_1:10;
          then r2+2*PI in ].PI,2*PI.[ by XXREAL_1:4;
          then sin.(r2+2*PI) < 0 by COMPTRIG:25;then
      A9: sin.r2 < 0 by SIN_COS:83;
          3/2*PI+2*PI*(-1) < r2 & r2 < 2*PI+2*PI*(-1)
          by A3,A4,A6,XXREAL_1:3;
          then sin r2 > -1 by SIN_COS6:39;
          then sin.r2 > -1 by SIN_COS:def 21;
          then (sin.r2)" < (-1)" by A9,XREAL_1:89;
          hence cosec.r2 < cosec.r1 by A4,A7,RFUNCT_1:def 8;
      end;
      suppose
      A10: -PI/2 < r1;
           then r1 in ].-PI/2,0.[ by A5,XXREAL_1:4;then
      A11: r1 in ].-PI/2,0.[ /\ dom cosec by A4,XBOOLE_0:def 3;
           -PI/2 < r2 by A3,A10,XXREAL_0:2;
           then r2 in ].-PI/2,0.[ by A5,XXREAL_1:4;
           then r2 in ].-PI/2,0.[ /\ dom cosec by A4,XBOOLE_0:def 3;
           hence cosec.r2 < cosec.r1 by A3,A11,Th15,RFUNCT_2:def 3;
      end;
    end;
    hence cosec.r2 < cosec.r1;
end;

theorem Th20:
  cosec is_decreasing_on ].0,PI/2.]
proof
    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 ].0,PI/2.] & r1 in dom cosec & r2 in ].0,PI/2.] & r2 in dom cosec
    by A1,A2,XBOOLE_0:def 3;then
A5: 0 < r1 & r1 <= PI/2 & 0 < r2 & r2 <= PI/2 by XXREAL_1:2;
    now per cases by A5,REAL_1:def 5;
      suppose
      A6: r2 < PI/2;
          then r1 < PI/2 by A3,XXREAL_0:2;
          then r1 in ].0,PI/2.[ by A5,XXREAL_1:4;then
      A7: r1 in ].0,PI/2.[ /\ dom cosec by A4,XBOOLE_0:def 3;
          r2 in ].0,PI/2.[ by A5,A6,XXREAL_1:4;
          then r2 in ].0,PI/2.[ /\ dom cosec by A4,XBOOLE_0:def 3;
          hence cosec.r2 < cosec.r1 by A3,A7,Th16,RFUNCT_2:def 3;
      end;
      suppose
      A8:  r2 = PI/2;
      A9:  cosec.r2 = 1/1 by A4,A8,RFUNCT_1:def 8,SIN_COS:81
           .= 1;
      A10: sin.r1 > 0 by A4,Lm4,COMPTRIG:23;
           sin r1 < 1 by A3,A5,A8,SIN_COS6:30;
           then sin.r1 < 1 by SIN_COS:def 21;
           then 1/1 < 1/sin.r1 by A10,XREAL_1:78;
           hence cosec.r2 < cosec.r1 by A4,A9,RFUNCT_1:def 8;
      end;
    end;
    hence cosec.r2 < cosec.r1;
end;

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

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

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

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

registration
  cluster sec | [.0,PI/2.[ -> one-to-one;
  coherence by Th17,FCONT_3:16;
  cluster sec | ].PI/2,PI.] -> one-to-one;
  coherence by Th18,FCONT_3:16;
  cluster cosec | [.-PI/2,0.[ -> one-to-one;
  coherence by Th19,FCONT_3:16;
  cluster cosec | ].0,PI/2.] -> one-to-one;
  coherence by Th20,FCONT_3:16;
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;

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

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

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

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

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

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

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

theorem Th28:
  rng arccosec2 = ].0,PI/2.]
proof
  dom (cosec|].0,PI/2.]) = ].0,PI/2.] by Th4,RELAT_1:91;
  hence thesis by FUNCT_1:55;
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;

definition let th be real number;
  redefine func sec th -> Real;
  coherence;
  redefine func cosec th -> Real;
  coherence;
end;

Lm9:
  0 in [.0,PI/2.[ & PI/4 in [.0,PI/2.[
proof
A3: PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;
    PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;
    hence thesis by A3,COMPTRIG:21;
end;

Lm10:
  3/4*PI in ].PI/2,PI.] & PI in ].PI/2,PI.]
proof
    PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;then
A2: PI/4+PI/2 > 0+PI/2 by XREAL_1:10;
    PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;then
    PI/4+PI/2 < PI/2+PI/2 by XREAL_1:10;
    hence thesis by A2,COMPTRIG:21;
end;

Lm11:
  -PI/2 in [.-PI/2,0.[ & -PI/4 in [.-PI/2,0.[
proof
A3: -PI/4 < -0;
    PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;
    then -PI/4 > -PI/2 by XREAL_1:26;
    hence thesis by A3,COMPTRIG:21;
end;

Lm12:
  PI/4 in ].0,PI/2.] & PI/2 in ].0,PI/2.]
proof
A2: PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;
    PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;
    hence thesis by A2,COMPTRIG:21;
end;

theorem Th29:
  sin.(PI/4) = 1/sqrt 2 & cos.(PI/4) = 1/sqrt 2
proof
A1: 1 = (sin.(PI/4))^2 + (sin.(PI/4))^2 by SIN_COS:31,SIN_COS:78
    .= 2*(sin.(PI/4))^2;
    (sqrt(1/2))^2 = 1/2 by SQUARE_1:def 4;then
A2: sin.(PI/4) = sqrt(1/2) or sin.(PI/4) = -sqrt(1/2) by A1,SQUARE_1:109;
A4: PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;
    PI/4 < PI/1 by COMPTRIG:21,REAL_2:200;then
A5: PI/4 in ].0,PI.[ by A4,XXREAL_1:4;
    sqrt(1/2) > 0 by SQUARE_1:93;then
    -sqrt(1/2) <= -0 by XREAL_1:26;
    hence thesis by A2,A5,COMPTRIG:23,SQUARE_1:101,SIN_COS:78;
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: sin.(-PI/4) = -1/sqrt 2 by Th29,SIN_COS:33;
A2: cos.(-PI/4) = 1/sqrt 2 by Th29,SIN_COS:33;
A3: sin.(3/4*PI) = sin.(PI+(-PI/4))
    .= -(-1/sqrt 2) by A1,SIN_COS:83
    .= 1/sqrt 2;
    cos.(3/4*PI) = cos.(PI+(-PI/4))
    .= -1/sqrt 2 by A2,SIN_COS:83;
    hence thesis by A3,Th29,SIN_COS:33;
end;

theorem Th31:
  sec.0 = 1 & sec.(PI/4) = sqrt 2 &
  sec.(3/4*PI) = -sqrt 2 & sec.PI = -1
proof
A2: sec.0 = 1/1 by Lm9,Th1,RFUNCT_1:def 8,SIN_COS:33
    .= 1;
A4: sec.(PI/4) = 1/(1/sqrt 2) by Lm9,Th1,RFUNCT_1:def 8,Th29
    .= sqrt 2;
A6: sec.(3/4*PI) = 1/(-1/sqrt 2) by Lm10,Th2,Th30,RFUNCT_1:def 8
    .= -1/(1/sqrt 2) by XCMPLX_1:189
    .= -sqrt 2;
    sec.PI = 1/(-1) by Lm10,Th2,RFUNCT_1:def 8,SIN_COS:81
    .= -1;
    hence thesis by A2,A4,A6;
end;

theorem Th32:
  cosec.(-PI/2) = -1 & cosec.(-PI/4) = -sqrt 2 &
  cosec.(PI/4) = sqrt 2 & cosec.(PI/2) = 1
proof
A2: cosec.(-PI/2) = 1/sin.(-PI/2) by Lm11,Th3,RFUNCT_1:def 8
    .= 1/(-1) by SIN_COS:33,SIN_COS:81
    .= -1;
A4: cosec.(-PI/4) = 1/(-1/sqrt 2) by Lm11,Th3,Th30,RFUNCT_1:def 8
    .= -1/(1/sqrt 2) by XCMPLX_1:189
    .= -sqrt 2;
A6: cosec.(PI/4) = 1/(1/sqrt 2) by Lm12,Th4,Th29,RFUNCT_1:def 8
    .= sqrt 2;
    cosec.(PI/2) = 1/1 by Lm12,Th4,RFUNCT_1:def 8,SIN_COS:81
    .= 1;
    hence thesis by A2,A4,A6;
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
A1: x in [.0,PI/4.];
A3: PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;
    then x in ].0,PI/4.[ \/ {0,PI/4} by A1,XXREAL_1:128;then
A4: x in ].0,PI/4.[ or x in {0,PI/4} by XBOOLE_0:def 2;
    per cases by A4,TARSKI:def 2;
      suppose
      A5:  x in ].0,PI/4.[;
      A6:  0 in [.0,PI/2.[ by COMPTRIG:21;
           PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;then
      AA:  PI/4 in [.0,PI/2.[ by A3;then
      A7:  [.0,PI/4.] c= [.0,PI/2.[ by A6,RCOMP_2:18;
      A8:  sec is_increasing_on [.0,PI/4.]
           by A6,AA,Th17,RCOMP_2:18,RFUNCT_2:60;
      A9:  0 in [.0,PI/4.] by A3,XXREAL_1:1;
      A10: [.0,PI/4.] /\ dom sec = [.0,PI/4.]
           by A7,Th1,XBOOLE_1:1,XBOOLE_1:28;
      A11: ].0,PI/4.[ c= [.0,PI/4.] by XXREAL_1:25;
           x in { s where s is Real: 0 < s & s < PI/4 }
           by A5,RCOMP_1:def 2;
           then ex s be Real st s=x & 0 < s & s < PI/4;then
      A12: 1 < sec.x by A5,A8,A9,A10,A11,Th31,RFUNCT_2:def 2;
           PI/4 in {s where s is Real: 0 <= s & s <= PI/4} by A3;then
      A13: PI/4 in [.0,PI/4.] /\ dom sec by A10,RCOMP_1:def 1;
           x in { s where s is Real: 0 < s & s < PI/4 }
           by A5,RCOMP_1:def 2;
           then ex s be Real st s=x & 0 < s & s < PI/4;
           then sec.x < sqrt 2 by A5,A8,A10,A11,A13,Th31,RFUNCT_2:def 2;then
      A14: sec.x in ].1,sqrt 2.[ by A12,XXREAL_1:4;
           ].1,sqrt 2.[ c= [.1,sqrt 2.] by XXREAL_1:25;
           hence sec.x in [.1,sqrt 2.] by A14;
      end;
      suppose x = 0;
        hence sec.x in [.1,sqrt 2.] by Th31,SQUARE_1:84,XXREAL_1:1;
      end;
      suppose x = PI/4;
        hence sec.x in [.1,sqrt 2.] by Th31,SQUARE_1:84,XXREAL_1:1;
      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;
    assume
A1: x in [.3/4*PI,PI.];
A3: PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;then
A4: PI/4+PI/2 < PI/2+PI/2 by XREAL_1:10;
    then x in ].3/4*PI,PI.[ \/ {3/4*PI,PI} by A1,XXREAL_1:128;then
A5: x in ].3/4*PI,PI.[ or x in {3/4*PI,PI} by XBOOLE_0:def 2;
    per cases by A5,TARSKI:def 2;
      suppose
      A6:  x in ].3/4*PI,PI.[;
           PI/4+PI/4 < PI/2+PI/4 by A3,XREAL_1:10;then
      A7:  3/4*PI in ].PI/2,PI.] by A4;
      AA:  PI in ].PI/2,PI.] by COMPTRIG:21;then
      A8:  [.3/4*PI,PI.] c= ].PI/2,PI.] by A7,RCOMP_2:19;
      A9:  sec is_increasing_on [.3/4*PI,PI.]
           by A7,AA,Th18,RCOMP_2:19,RFUNCT_2:60;
      A10: 3/4*PI in [.3/4*PI,PI.] by A4,XXREAL_1:1;
      A11: [.3/4*PI,PI.] /\ dom sec = [.3/4*PI,PI.]
           by A8,Th2,XBOOLE_1:1,XBOOLE_1:28;
      A12: ].3/4*PI,PI.[ c= [.3/4*PI,PI.] by XXREAL_1:25;
           x in { s where s is Real: 3/4*PI < s & s < PI }
           by A6,RCOMP_1:def 2;
           then ex s be Real st s=x & 3/4*PI < s & s < PI;then
      A13: -sqrt 2 < sec.x by A6,A9,A10,A11,A12,Th31,RFUNCT_2:def 2;
           PI in {s where s is Real: 3/4*PI <= s & s <= PI} by A4;then
      A14: PI in [.3/4*PI,PI.] /\ dom sec by A11,RCOMP_1:def 1;
           x in { s where s is Real: 3/4*PI < s & s < PI }
           by A6,RCOMP_1:def 2;
           then ex s be Real st s=x & 3/4*PI < s & s < PI;
           then sec.x < -1 by A6,A9,A11,A12,A14,Th31,RFUNCT_2:def 2;then
      A15: sec.x in ].-sqrt 2,-1.[ by A13,XXREAL_1:4;
           ].-sqrt 2,-1.[ c= [.-sqrt 2,-1.] by XXREAL_1:25;
           hence sec.x in [.-sqrt 2,-1.] by A15;
      end;
      suppose
      A16: x = 3/4*PI;
           -sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
           hence sec.x in [.-sqrt 2,-1.] by A16,Th31,XXREAL_1:1;
      end;
      suppose
      A17: x = PI;
           -sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
           hence sec.x in [.-sqrt 2,-1.] by A17,Th31,XXREAL_1:1;
      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;
    assume
A1: x in [.-PI/2,-PI/4.];
    PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;then
A3: -PI/2 < -PI/4 by XREAL_1:26;
    then x in ].-PI/2,-PI/4.[ \/ {-PI/2,-PI/4} by A1,XXREAL_1:128;then
A4: x in ].-PI/2,-PI/4.[ or x in {-PI/2,-PI/4} by XBOOLE_0:def 2;
    per cases by A4,TARSKI:def 2;
      suppose
      A5:  x in ].-PI/2,-PI/4.[;
      A6:  -PI/2 in [.-PI/2,0.[ by COMPTRIG:21;
           -PI/4 < -0;then
      AA:  -PI/4 in [.-PI/2,0.[ by A3;then
      A7:  [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by A6,RCOMP_2:18;
      A8:  cosec is_decreasing_on [.-PI/2,-PI/4.]
           by A6,AA,Th19,RCOMP_2:18,RFUNCT_2:61;
      A9:  -PI/2 in [.-PI/2,-PI/4.] by A3,XXREAL_1:1;
      A10: [.-PI/2,-PI/4.] /\ dom cosec = [.-PI/2,-PI/4.]
           by A7,Th3,XBOOLE_1:1,XBOOLE_1:28;
      A11: ].-PI/2,-PI/4.[ c= [.-PI/2,-PI/4.] by XXREAL_1:25;
           x in { s where s is Real: -PI/2 < s & s < -PI/4 }
           by A5,RCOMP_1:def 2;
           then ex s be Real st s=x & -PI/2 < s & s < -PI/4;then
      A12: -1 > cosec.x by A5,A8,A9,A10,A11,Th32,RFUNCT_2:def 3;
           -PI/4 in {s where s is Real: -PI/2 <= s & s <= -PI/4} by A3;then
      A13: -PI/4 in [.-PI/2,-PI/4.] /\ dom cosec by A10,RCOMP_1:def 1;
           x in { s where s is Real: -PI/2 < s & s < -PI/4 }
           by A5,RCOMP_1:def 2;
           then ex s be Real st s=x & -PI/2 < s & s < -PI/4;
           then cosec.x > -sqrt 2 by A5,A8,A10,A11,A13,Th32,RFUNCT_2:def 3;then
      A14: cosec.x in ].-sqrt 2,-1.[ by A12,XXREAL_1:4;
           ].-sqrt 2,-1.[ c= [.-sqrt 2,-1.] by XXREAL_1:25;
           hence cosec.x in [.-sqrt 2,-1.] by A14;
      end;
      suppose
      A15: x = -PI/2;
           -sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
           hence cosec.x in [.-sqrt 2,-1.] by A15,Th32,XXREAL_1:1;
      end;
      suppose
      A16: x = -PI/4;
           -sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
           hence cosec.x in [.-sqrt 2,-1.] by A16,Th32,XXREAL_1:1;
      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;
    assume
A1: x in [.PI/4,PI/2.];
A3: PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;
    then x in ].PI/4,PI/2.[ \/ {PI/4,PI/2} by A1,XXREAL_1:128;then
A4: x in ].PI/4,PI/2.[ or x in {PI/4,PI/2} by XBOOLE_0:def 2;
    per cases by A4,TARSKI:def 2;
      suppose
      A5:  x in ].PI/4,PI/2.[;
           PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;then
      A6:  PI/4 in ].0,PI/2.] by A3;
      AA:  PI/2 in ].0,PI/2.] by COMPTRIG:21;then
      A7:  [.PI/4,PI/2.] c= ].0,PI/2.] by A6,RCOMP_2:19;
      A8:  cosec is_decreasing_on [.PI/4,PI/2.]
           by A6,AA,Th20,RCOMP_2:19,RFUNCT_2:61;
      A9:  PI/4 in [.PI/4,PI/2.] by A3,XXREAL_1:1;
      A10: [.PI/4,PI/2.] /\ dom cosec = [.PI/4,PI/2.]
           by A7,Th4,XBOOLE_1:1,XBOOLE_1:28;
      A11: ].PI/4,PI/2.[ c= [.PI/4,PI/2.] by XXREAL_1:25;
           x in { s where s is Real: PI/4 < s & s < PI/2 }
           by A5,RCOMP_1:def 2;
           then ex s be Real st s=x & PI/4 < s & s < PI/2;then
      A12: sqrt 2 > cosec.x by A5,A8,A9,A10,A11,Th32,RFUNCT_2:def 3;
           PI/2 in {s where s is Real: PI/4 <= s & s <= PI/2} by A3;then
      A13: PI/2 in [.PI/4,PI/2.] /\ dom cosec by A10,RCOMP_1:def 1;
           x in { s where s is Real: PI/4 < s & s < PI/2 }
           by A5,RCOMP_1:def 2;
           then ex s be Real st s=x & PI/4 < s & s < PI/2;
           then cosec.x > 1 by A5,A8,A10,A11,A13,Th32,RFUNCT_2:def 3;then
      A14: cosec.x in ].1,sqrt 2.[ by A12,XXREAL_1:4;
           ].1,sqrt 2.[ c= [.1,sqrt 2.] by XXREAL_1:25;
           hence cosec.x in [.1,sqrt 2.] by A14;
      end;
      suppose x = PI/4;
        hence cosec.x in [.1,sqrt 2.] by Th32,SQUARE_1:84,XXREAL_1:1;
      end;
      suppose x = PI/2;
        hence cosec.x in [.1,sqrt 2.] by Th32,SQUARE_1:84,XXREAL_1:1;
      end;
end;

Lm13:
  dom (sec | [.0,PI/4.]) = [.0,PI/4.]
proof
  [.0,PI/4.] c= [.0,PI/2.[ by Lm9,RCOMP_2:18;
  hence thesis by Th1,XBOOLE_1:1,RELAT_1:91;
end;

Lm14:
  dom (sec | [.3/4*PI,PI.]) = [.3/4*PI,PI.]
proof
  [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm10,RCOMP_2:19;
  hence thesis by Th2,XBOOLE_1:1,RELAT_1:91;
end;

Lm15:
  dom (cosec | [.-PI/2,-PI/4.]) = [.-PI/2,-PI/4.]
proof
  [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm11,RCOMP_2:18;
  hence thesis by Th3,XBOOLE_1:1,RELAT_1:91;
end;

Lm16:
  dom (cosec | [.PI/4,PI/2.]) = [.PI/4,PI/2.]
proof
  [.PI/4,PI/2.] c= ].0,PI/2.] by Lm12,RCOMP_2:19;
  hence thesis by Th4,XBOOLE_1:1,RELAT_1:91;
end;

Lm17:
  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:90;
  then dom (sec|[.0,PI/2.[) = [.0,PI/2.[ by Th1,XBOOLE_1:28;
  hence thesis by FUNCT_1:68;
end;

Lm18:
  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:90;
  then dom (sec|].PI/2,PI.]) = ].PI/2,PI.] by Th2,XBOOLE_1:28;
  hence thesis by FUNCT_1:68;
end;

Lm19:
  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:90;
  then dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ by Th3,XBOOLE_1:28;
  hence thesis by FUNCT_1:68;
end;

Lm20:
  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:90;
  then dom (cosec|].0,PI/2.]) = ].0,PI/2.] by Th4,XBOOLE_1:28;
  hence thesis by FUNCT_1:68;
end;

theorem Th37:
  sec is_continuous_on [.0,PI/2.[
proof
  for th be real number st th in [.0,PI/2.[ holds
  sec|[.0,PI/2.[ is_continuous_in th
  proof
      let th be real number such that
  A0: th in [.0,PI/2.[;
  A1: cos.th <> 0 by A0,Lm1,COMPTRIG:27;
  AA: cos is_differentiable_in th by SIN_COS:68;
  A2: sec is_continuous_in th by A1,AA,FDIFF_1:32,FCONT_1:10;
      th in dom (sec|[.0,PI/2.[) &
      for rseq st rng rseq c= dom (sec|[.0,PI/2.[) &
      rseq is convergent & lim rseq = th holds
      (sec|[.0,PI/2.[)*rseq is convergent &
      (sec|[.0,PI/2.[).th = lim((sec|[.0,PI/2.[)*rseq)
      proof
        now let rseq;
            assume
        A3: rng rseq c= dom (sec|[.0,PI/2.[) &
            rseq is convergent & lim rseq = th;
        A4: dom (sec|[.0,PI/2.[) = [.0,PI/2.[ by Th1,RELAT_1:91;then
            rng rseq c= dom sec by A3,Th1,XBOOLE_1:1;then
        A6: sec*rseq is convergent & sec.th = lim(sec*rseq)
            by A2,A3,FCONT_1:def 1;
            (sec|[.0,PI/2.[)*rseq = sec*rseq
            proof
              now let n be Element of NAT;
                  dom (rseq) = NAT by SEQ_1:3;
                  then rseq.n in rng rseq by FUNCT_1:def 5;then
              A7: (sec|[.0,PI/2.[).(rseq.n) = sec.(rseq.n) by A3,A4,FUNCT_1:72;
                  (sec|[.0,PI/2.[).(rseq.n) = ((sec|[.0,PI/2.[)*rseq).n
                  by A3,RFUNCT_2:21;
                  hence ((sec|[.0,PI/2.[)*rseq).n = (sec*rseq).n
                  by A3,A4,A7,Th1,XBOOLE_1:1,RFUNCT_2:21;
              end;
              hence thesis by FUNCT_2:113;
            end;
            hence (sec|[.0,PI/2.[)*rseq is convergent &
            (sec|[.0,PI/2.[).th = lim((sec|[.0,PI/2.[)*rseq) by A0,A6,Lm17;
        end;
        hence thesis by A0,Lm17;
      end;
      hence thesis by FCONT_1:def 1;
  end;
  hence sec is_continuous_on [.0,PI/2.[ by Th1,FCONT_1:def 2;
end;

theorem Th38:
  sec is_continuous_on ].PI/2,PI.]
proof
  for th be real number st th in ].PI/2,PI.] holds
  sec|].PI/2,PI.] is_continuous_in th
  proof
      let th be real number such that
  A0: th in ].PI/2,PI.];
  A1: cos.th <> 0 by A0,Lm2,COMPTRIG:29;
  AA: cos is_differentiable_in th by SIN_COS:68;
  A2: sec is_continuous_in th by A1,AA,FDIFF_1:32,FCONT_1:10;
      th in dom (sec|].PI/2,PI.]) &
      for rseq st rng rseq c= dom (sec|].PI/2,PI.]) &
      rseq is convergent & lim rseq = th holds
      (sec|].PI/2,PI.])*rseq is convergent &
      (sec|].PI/2,PI.]).th = lim((sec|].PI/2,PI.])*rseq)
      proof
        now let rseq;
            assume
        A3: rng rseq c= dom (sec|].PI/2,PI.]) &
            rseq is convergent & lim rseq = th;
        A4: dom (sec|].PI/2,PI.]) = ].PI/2,PI.] by Th2,RELAT_1:91;then
            rng rseq c= dom sec by A3,Th2,XBOOLE_1:1;then
        A6: sec*rseq is convergent & sec.th = lim(sec*rseq)
            by A2,A3,FCONT_1:def 1;
            (sec|].PI/2,PI.])*rseq = sec*rseq
            proof
              now let n be Element of NAT;
                  dom (rseq) = NAT by SEQ_1:3;
                  then rseq.n in rng rseq by FUNCT_1:def 5;then
              A7: (sec|].PI/2,PI.]).(rseq.n) = sec.(rseq.n)
                  by A3,A4,FUNCT_1:72;
                  (sec|].PI/2,PI.]).(rseq.n) = ((sec|].PI/2,PI.])*rseq).n
                  by A3,RFUNCT_2:21;
                  hence ((sec|].PI/2,PI.])*rseq).n = (sec*rseq).n
                  by A3,A4,A7,Th2,XBOOLE_1:1,RFUNCT_2:21;
              end;
              hence thesis by FUNCT_2:113;
            end;
            hence (sec|].PI/2,PI.])*rseq is convergent &
            (sec|].PI/2,PI.]).th = lim((sec|].PI/2,PI.])*rseq) by A0,A6,Lm18;
        end;
        hence thesis by A0,Lm18;
      end;
      hence thesis by FCONT_1:def 1;
  end;
  hence sec is_continuous_on ].PI/2,PI.] by Th2,FCONT_1:def 2;
end;

theorem Th39:
  cosec is_continuous_on [.-PI/2,0.[
proof
  for th be real number st th in [.-PI/2,0.[ holds
  cosec|[.-PI/2,0.[ is_continuous_in th
  proof
      let th be real number such that
  A0: th in [.-PI/2,0.[;
      -PI < th & th < 0 by A0,Lm3,XXREAL_1:4;
      then -PI+2*PI < th+2*PI & th+2*PI < 0+2*PI by XREAL_1:10;
      then th+2*PI in ].PI,2*PI.[ by XXREAL_1:4;
      then sin.(th+2*PI) <> 0 by COMPTRIG:25;then
  A1: sin.th <> 0 by SIN_COS:83;
  AA: sin is_differentiable_in th by SIN_COS:69;
  A2: cosec is_continuous_in th by A1,AA,FDIFF_1:32,FCONT_1:10;
      th in dom (cosec|[.-PI/2,0.[) &
      for rseq st rng rseq c= dom (cosec|[.-PI/2,0.[) &
      rseq is convergent & lim rseq = th holds
      (cosec|[.-PI/2,0.[)*rseq is convergent &
      (cosec|[.-PI/2,0.[).th = lim((cosec|[.-PI/2,0.[)*rseq)
      proof
        now let rseq;
            assume
        A3: rng rseq c= dom (cosec|[.-PI/2,0.[) &
            rseq is convergent & lim rseq = th;
        A4: dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ by Th3,RELAT_1:91;then
            rng rseq c= dom cosec by A3,Th3,XBOOLE_1:1;then
        A6: cosec*rseq is convergent & cosec.th = lim(cosec*rseq)
            by A2,A3,FCONT_1:def 1;
            (cosec|[.-PI/2,0.[)*rseq = cosec*rseq
            proof
              now let n be Element of NAT;
                  dom (rseq) = NAT by SEQ_1:3;
                  then rseq.n in rng rseq by FUNCT_1:def 5;then
              A7: (cosec|[.-PI/2,0.[).(rseq.n) = cosec.(rseq.n)
                  by A3,A4,FUNCT_1:72;
                  (cosec|[.-PI/2,0.[).(rseq.n) = ((cosec|[.-PI/2,0.[)*rseq).n
                  by A3,RFUNCT_2:21;
                  hence ((cosec|[.-PI/2,0.[)*rseq).n = (cosec*rseq).n
                  by A3,A4,A7,Th3,XBOOLE_1:1,RFUNCT_2:21;
              end;
              hence thesis by FUNCT_2:113;
            end;
            hence (cosec|[.-PI/2,0.[)*rseq is convergent &
            (cosec|[.-PI/2,0.[).th = lim((cosec|[.-PI/2,0.[)*rseq)
            by A0,A6,Lm19;
        end;
        hence thesis by A0,Lm19;
      end;
      hence thesis by FCONT_1:def 1;
  end;
  hence cosec is_continuous_on [.-PI/2,0.[ by Th3,FCONT_1:def 2;
end;

theorem Th40:
  cosec is_continuous_on ].0,PI/2.]
proof
  for th be real number st th in ].0,PI/2.] holds
  cosec|].0,PI/2.] is_continuous_in th
  proof
      let th be real number such that
  A0: th in ].0,PI/2.];
  A1: sin.th <> 0 by A0,Lm4,COMPTRIG:23;
  AA: sin is_differentiable_in th by SIN_COS:69;
  A2: cosec is_continuous_in th by A1,AA,FDIFF_1:32,FCONT_1:10;
      th in dom (cosec|].0,PI/2.]) &
      for rseq st rng rseq c= dom (cosec|].0,PI/2.]) &
      rseq is convergent & lim rseq = th holds
      (cosec|].0,PI/2.])*rseq is convergent &
      (cosec|].0,PI/2.]).th = lim((cosec|].0,PI/2.])*rseq)
      proof
        now let rseq;
            assume
        A3: rng rseq c= dom (cosec|].0,PI/2.]) &
            rseq is convergent & lim rseq = th;
        A4: dom (cosec|].0,PI/2.]) = ].0,PI/2.] by Th4,RELAT_1:91;then
            rng rseq c= dom cosec by A3,Th4,XBOOLE_1:1;then
        A6: cosec*rseq is convergent & cosec.th = lim(cosec*rseq)
            by A2,A3,FCONT_1:def 1;
            (cosec|].0,PI/2.])*rseq = cosec*rseq
            proof
              now let n be Element of NAT;
                  dom (rseq) = NAT by SEQ_1:3;
                  then rseq.n in rng rseq by FUNCT_1:def 5;then
              A7: (cosec|].0,PI/2.]).(rseq.n) = cosec.(rseq.n)
                  by A3,A4,FUNCT_1:72;
                  (cosec|].0,PI/2.]).(rseq.n) = ((cosec|].0,PI/2.])*rseq).n
                  by A3,RFUNCT_2:21;
                  hence ((cosec|].0,PI/2.])*rseq).n = (cosec*rseq).n
                  by A3,A4,A7,Th4,XBOOLE_1:1,RFUNCT_2:21;
              end;
              hence thesis by FUNCT_2:113;
            end;
            hence (cosec|].0,PI/2.])*rseq is convergent &
            (cosec|].0,PI/2.]).th = lim((cosec|].0,PI/2.])*rseq)
            by A0,A6,Lm20;
        end;
        hence thesis by A0,Lm20;
      end;
      hence thesis by FCONT_1:def 1;
  end;
  hence cosec is_continuous_on ].0,PI/2.] by Th4,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;
    A2: PI/4 >= 0 by Lm9,XXREAL_1:3;
    A4: sec is_continuous_on [.0,PI/4.]
        by Lm9,Th37,RCOMP_2:18,FCONT_1:17;
        y1 in [.sec.0,sec.(PI/4).] \/ [.sec.(PI/4),sec.0.]
        by A1,Th31,XBOOLE_0:def 2;
        then consider x be Real such that
    A5: x in [.0,PI/4.] and
    A6: y1 = sec.x by A2,A4,FCONT_2:16;
        take x;
        thus x in dom (sec | [.0,PI/4.]) & y = (sec | [.0,PI/4.]).x
        by A5,A6,Lm13,FUNCT_1:72;
    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
    A7: x in dom (sec | [.0,PI/4.]) and
    A8: y = (sec | [.0,PI/4.]).x;
        reconsider x1=x as Real by A7;
        y = sec.x1 by A7,A8,Lm13,FUNCT_1:72;
        hence y in [.1,sqrt 2.] by A7,Lm13,Th33;
    end;
  end;
  hence thesis by FUNCT_1:def 5;
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
        assume
    A1: y in [.-sqrt 2,-1.];
        then reconsider y1=y as Real;
    A2: 3/4*PI <= PI by Lm10,XXREAL_1:2;
    A4: sec is_continuous_on [.3/4*PI,PI.]
        by Lm10,Th38,RCOMP_2:19,FCONT_1:17;
        y1 in [.sec.(3/4*PI),sec.PI.] \/ [.sec.PI,sec.(3/4*PI).]
        by A1,Th31,XBOOLE_0:def 2;
        then consider x be Real such that
    A5: x in [.3/4*PI,PI.] and
    A6: y1 = sec.x by A2,A4,FCONT_2:16;
        take x;
        thus x in dom (sec | [.3/4*PI,PI.]) & y = (sec | [.3/4*PI,PI.]).x
        by A5,A6,Lm14,FUNCT_1:72;
    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
    A7: x in dom (sec | [.3/4*PI,PI.]) and
    A8: y = (sec | [.3/4*PI,PI.]).x;
        reconsider x1=x as Real by A7;
        y = sec.x1 by A7,A8,Lm14,FUNCT_1:72;
        hence y in [.-sqrt 2,-1.] by A7,Lm14,Th34;
    end;
  end;
  hence thesis by FUNCT_1:def 5;
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
      assume
  A1: y in [.-sqrt 2,-1.];
      then reconsider y1=y as Real;
  A2: -PI/2 <= -PI/4 by Lm11,XXREAL_1:3;
  A4: cosec is_continuous_on [.-PI/2,-PI/4.]
      by Lm11,Th39,RCOMP_2:18,FCONT_1:17;
      y1 in [.cosec.(-PI/4),cosec.(-PI/2).] \/
      [.cosec.(-PI/2),cosec.(-PI/4).] by A1,Th32,XBOOLE_0:def 2;
      then consider x be Real such that
  A5: x in [.-PI/2,-PI/4.] and
  A6: y1 = cosec.x by A2,A4,FCONT_2:16;
      take x;
      thus x in dom (cosec | [.-PI/2,-PI/4.]) &
      y = (cosec | [.-PI/2,-PI/4.]).x by A5,A6,Lm15,FUNCT_1:72;
    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
  A7: x in dom (cosec | [.-PI/2,-PI/4.]) and
  A8: y = (cosec | [.-PI/2,-PI/4.]).x;
      reconsider x1=x as Real by A7;
      y = cosec.x1 by A7,A8,Lm15,FUNCT_1:72;
      hence y in [.-sqrt 2,-1.] by A7,Lm15,Th35;
    end;
  end;
  hence thesis by FUNCT_1:def 5;
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
      assume
  A1: y in [.1,sqrt 2.];
      then reconsider y1=y as Real;
  A2: PI/4 <= PI/2 by Lm12,XXREAL_1:2;
  A4: cosec is_continuous_on [.PI/4,PI/2.]
      by Lm12,Th40,RCOMP_2:19,FCONT_1:17;
      y1 in [.cosec.(PI/2),cosec.(PI/4).] \/
      [.cosec.(PI/4),cosec.(PI/2).] by A1,Th32,XBOOLE_0:def 2;
      then consider x be Real such that
  A5: x in [.PI/4,PI/2.] and
  A6: y1 = cosec.x by A2,A4,FCONT_2:16;
      take x;
      thus x in dom (cosec | [.PI/4,PI/2.]) &
      y = (cosec | [.PI/4,PI/2.]).x by A5,A6,Lm16,FUNCT_1:72;
    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
  A7: x in dom (cosec | [.PI/4,PI/2.]) and
  A8: y = (cosec | [.PI/4,PI/2.]).x;
      reconsider x1=x as Real by A7;
      y = cosec.x1 by A7,A8,Lm16,FUNCT_1:72;
      hence y in [.1,sqrt 2.] by A7,Lm16,Th36;
    end;
  end;
  hence thesis by FUNCT_1:def 5;
end;

theorem Th45:
  [.1,sqrt 2.] c= dom arcsec1
proof
A1: [.0,PI/4.] c= [.0,PI/2.[ by Lm9,RCOMP_2:18;
A2: 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:148;
      then consider x be set such that
  A3: x in dom sec and
  A4: x in [.0,PI/4.] and
  A5: y = sec.x by FUNCT_1:def 12;
      y in sec.:[.0,PI/2.[ by A1,A3,A4,A5,FUNCT_1:def 12;
      hence thesis by RELAT_1:148;
    end;
    thus [.1,sqrt 2.] c= dom arcsec1 by A2,Th41,FUNCT_1:55;
end;

theorem Th46:
  [.-sqrt 2,-1.] c= dom arcsec2
proof
A1: [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm10,RCOMP_2:19;
A2: 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:148;
      then consider x be set such that
  A3: x in dom sec and
  A4: x in [.3/4*PI,PI.] and
  A5: y = sec.x by FUNCT_1:def 12;
      y in sec.:].PI/2,PI.] by A1,A3,A4,A5,FUNCT_1:def 12;
      hence thesis by RELAT_1:148;
    end;
    thus [.-sqrt 2,-1.] c= dom arcsec2 by A2,Th42,FUNCT_1:55;
end;

theorem Th47:
  [.-sqrt 2,-1.] c= dom arccosec1
proof
A1: [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm11,RCOMP_2:18;
A2: 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:148;
      then consider x be set such that
  A3: x in dom cosec and
  A4: x in [.-PI/2,-PI/4.] and
  A5: y = cosec.x by FUNCT_1:def 12;
      y in cosec.:[.-PI/2,0.[ by A1,A3,A4,A5,FUNCT_1:def 12;
      hence thesis by RELAT_1:148;
    end;
    thus [.-sqrt 2,-1.] c= dom arccosec1 by A2,Th43,FUNCT_1:55;
end;

theorem Th48:
  [.1,sqrt 2.] c= dom arccosec2
proof
A1: [.PI/4,PI/2.] c= ].0,PI/2.] by Lm12,RCOMP_2:19;
A2: 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:148;
      then consider x be set such that
  A3: x in dom cosec and
  A4: x in [.PI/4,PI/2.] and
  A5: y = cosec.x by FUNCT_1:def 12;
      y in cosec.:].0,PI/2.] by A1,A3,A4,A5,FUNCT_1:def 12;
      hence thesis by RELAT_1:148;
    end;
    thus [.1,sqrt 2.] c= dom arccosec2 by A2,Th44,FUNCT_1:55;
end;

Lm21:
  sec | [.0,PI/4.] is_increasing_on [.0,PI/4.]
proof
  sec is_increasing_on [.0,PI/4.]
  by Lm9,Th17,RCOMP_2:18,RFUNCT_2:60;
  hence thesis by RFUNCT_2:50;
end;

Lm22:
  sec | [.3/4*PI,PI.] is_increasing_on [.3/4*PI,PI.]
proof
  sec is_increasing_on [.3/4*PI,PI.]
  by Lm10,Th18,RCOMP_2:19,RFUNCT_2:60;
  hence thesis by RFUNCT_2:50;
end;

Lm23:
  cosec | [.-PI/2,-PI/4.] is_decreasing_on [.-PI/2,-PI/4.]
proof
  cosec is_decreasing_on [.-PI/2,-PI/4.]
  by Lm11,Th19,RCOMP_2:18,RFUNCT_2:61;
  hence thesis by RFUNCT_2:51;
end;

Lm24:
  cosec | [.PI/4,PI/2.] is_decreasing_on [.PI/4,PI/2.]
proof
  cosec is_decreasing_on [.PI/4,PI/2.]
  by Lm12,Th20,RCOMP_2:19,RFUNCT_2:61;
  hence thesis by RFUNCT_2:51;
end;

Lm25:
  sec | [.0,PI/4.] is one-to-one
proof
  (sec | [.0,PI/2.[) | [.0,PI/4.] = sec | [.0,PI/4.]
  by Lm9,RCOMP_2:18,RELAT_1:103;
  hence sec | [.0,PI/4.] is one-to-one;
end;

Lm26:
  sec | [.3/4*PI,PI.] is one-to-one
proof
  (sec | ].PI/2,PI.]) | [.3/4*PI,PI.] = sec | [.3/4*PI,PI.]
  by Lm10,RCOMP_2:19,RELAT_1:103;
  hence sec | [.3/4*PI,PI.] is one-to-one;
end;

Lm27:
  cosec | [.-PI/2,-PI/4.] is one-to-one
proof
  (cosec | [.-PI/2,0.[) | [.-PI/2,-PI/4.] = cosec | [.-PI/2,-PI/4.]
  by Lm11,RCOMP_2:18,RELAT_1:103;
  hence cosec | [.-PI/2,-PI/4.] is one-to-one;
end;

Lm28:
  cosec | [.PI/4,PI/2.] is one-to-one
proof
  (cosec | ].0,PI/2.]) | [.PI/4,PI/2.] = cosec | [.PI/4,PI/2.]
  by Lm12,RCOMP_2:19,RELAT_1:103;
  hence cosec | [.PI/4,PI/2.] is one-to-one;
end;

registration
  cluster sec | [.0,PI/4.] -> one-to-one;
  coherence by Lm25;
  cluster sec | [.3/4*PI,PI.] -> one-to-one;
  coherence by Lm26;
  cluster cosec | [.-PI/2,-PI/4.] -> one-to-one;
  coherence by Lm27;
  cluster cosec | [.PI/4,PI/2.] -> one-to-one;
  coherence by Lm28;
end;

theorem Th49:
  arcsec1 | [.1,sqrt 2.] = (sec | [.0,PI/4.])"
proof
    set h = sec | [.0,PI/2.[;
    (sec | [.0,PI/4.])" = (h | [.0,PI/4.])"
    by Lm9,RCOMP_2:18,RELAT_1:103
    .= h" | (h.:[.0,PI/4.]) by RFUNCT_2:40
    .= h" | rng (h | [.0,PI/4.]) by RELAT_1:148
    .= h" | ([.1,sqrt 2.]) by Th41,Lm9,RCOMP_2:18,RELAT_1:103;
    hence (sec | [.0,PI/4.])" = arcsec1 | [.1,sqrt 2.];
end;

theorem Th50:
  arcsec2 | [.-sqrt 2,-1.] = (sec | [.3/4*PI,PI.])"
proof
    set h = sec | ].PI/2,PI.];
    (sec | [.3/4*PI,PI.])" = (h | [.3/4*PI,PI.])"
    by Lm10,RCOMP_2:19,RELAT_1:103
    .= h" | (h.:[.3/4*PI,PI.]) by RFUNCT_2:40
    .= h" | rng (h | [.3/4*PI,PI.]) by RELAT_1:148
    .= h" | ([.-sqrt 2,-1.]) by Th42,Lm10,RCOMP_2:19,RELAT_1:103;
    hence (sec | [.3/4*PI,PI.])" = arcsec2 | [.-sqrt 2,-1.];
end;

theorem Th51:
  arccosec1 | [.-sqrt 2,-1.] = (cosec | [.-PI/2,-PI/4.])"
proof
    set h = cosec | [.-PI/2,0.[;
    (cosec | [.-PI/2,-PI/4.])" = (h | [.-PI/2,-PI/4.])"
    by Lm11,RCOMP_2:18,RELAT_1:103
    .= h" | (h.:[.-PI/2,-PI/4.]) by RFUNCT_2:40
    .= h" | rng (h | [.-PI/2,-PI/4.]) by RELAT_1:148
    .= h" | ([.-sqrt 2,-1.]) by Th43,Lm11,RCOMP_2:18,RELAT_1:103;
    hence (cosec | [.-PI/2,-PI/4.])" = arccosec1 | [.-sqrt 2,-1.];
end;

theorem Th52:
  arccosec2 | [.1,sqrt 2.] = (cosec | [.PI/4,PI/2.])"
proof
    set h = cosec | ].0,PI/2.];
    (cosec | [.PI/4,PI/2.])" = (h | [.PI/4,PI/2.])"
    by Lm12,RCOMP_2:19,RELAT_1:103
    .= h" | (h.:[.PI/4,PI/2.]) by RFUNCT_2:40
    .= h" | rng (h | [.PI/4,PI/2.]) by RELAT_1:148
    .= h" | ([.1,sqrt 2.]) by Th44,Lm12,RCOMP_2:19,RELAT_1:103;
    hence (cosec | [.PI/4,PI/2.])" = arccosec2 | [.1,sqrt 2.];
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Th77:
  arcsec1 is_increasing_on sec.:[.0,PI/2.[
proof
    set f = sec | [.0,PI/2.[;
A1: f|[.0,PI/2.[ = f by RELAT_1:102;
A2: f is_increasing_on [.0,PI/2.[ by Th17,RFUNCT_2:50;
    f.:[.0,PI/2.[ = rng(f|[.0,PI/2.[) by RELAT_1:148
                 .= rng(sec|[.0,PI/2.[) by RELAT_1:102
                 .= sec.:[.0,PI/2.[ by RELAT_1:148;
    hence arcsec1 is_increasing_on sec.:[.0,PI/2.[ by A1,A2,FCONT_3:17;
end;

theorem Th78:
  arcsec2 is_increasing_on sec.:].PI/2,PI.]
proof
    set f = sec | ].PI/2,PI.];
A1: f|].PI/2,PI.] = f by RELAT_1:102;
A2: f is_increasing_on ].PI/2,PI.] by Th18,RFUNCT_2:50;
    f.:].PI/2,PI.] = rng(f|].PI/2,PI.]) by RELAT_1:148
                  .= rng(sec|].PI/2,PI.]) by RELAT_1:102
                  .= sec.:].PI/2,PI.] by RELAT_1:148;
    hence arcsec2 is_increasing_on sec.:].PI/2,PI.] by A1,A2,FCONT_3:17;
end;

theorem Th79:
  arccosec1 is_decreasing_on cosec.:[.-PI/2,0.[
proof
    set f = cosec | [.-PI/2,0.[;
A1: f|[.-PI/2,0.[ = f by RELAT_1:102;
A2: f is_decreasing_on [.-PI/2,0.[ by Th19,RFUNCT_2:51;
    f.:[.-PI/2,0.[ = rng(f|[.-PI/2,0.[) by RELAT_1:148
                  .= rng(cosec|[.-PI/2,0.[) by RELAT_1:102
                  .= cosec.:[.-PI/2,0.[ by RELAT_1:148;
    hence arccosec1 is_decreasing_on cosec.:[.-PI/2,0.[ by A1,A2,FCONT_3:18;
end;

theorem Th80:
  arccosec2 is_decreasing_on cosec.:].0,PI/2.]
proof
    set f = cosec | ].0,PI/2.];
A1: f|].0,PI/2.] = f by RELAT_1:102;
A2: f is_decreasing_on ].0,PI/2.] by Th20,RFUNCT_2:51;
    f.:].0,PI/2.] = rng(f|].0,PI/2.]) by RELAT_1:148
                 .= rng(cosec|].0,PI/2.]) by RELAT_1:102
                 .= cosec.:].0,PI/2.] by RELAT_1:148;
    hence arccosec2 is_decreasing_on cosec.:].0,PI/2.] by A1,A2,FCONT_3:18;
end;

theorem Th81:
  arcsec1 is_increasing_on [.1,sqrt 2.]
proof
A1: [.1,sqrt 2.] = sec.:[.0,PI/4.] by Th41,RELAT_1:148;
    [.1,sqrt 2.] c= sec.:[.0,PI/2.[ by A1,Lm9,RCOMP_2:18,RELAT_1:156;
    hence arcsec1 is_increasing_on [.1,sqrt 2.] by Th77,RFUNCT_2:60;
end;

theorem Th82:
  arcsec2 is_increasing_on [.-sqrt 2,-1.]
proof
A1: [.-sqrt 2,-1.] = sec.:[.3/4*PI,PI.] by Th42,RELAT_1:148;
    [.-sqrt 2,-1.] c= sec.:].PI/2,PI.] by A1,RELAT_1:156,Lm10,RCOMP_2:19;
    hence arcsec2 is_increasing_on [.-sqrt 2,-1.] by Th78,RFUNCT_2:60;
end;

theorem Th83:
  arccosec1 is_decreasing_on [.-sqrt 2,-1.]
proof
A1: [.-sqrt 2,-1.] = cosec.:[.-PI/2,-PI/4.] by Th43,RELAT_1:148;
    [.-sqrt 2,-1.] c= cosec.:[.-PI/2,0.[ by A1,Lm11,RCOMP_2:18,RELAT_1:156;
    hence arccosec1 is_decreasing_on [.-sqrt 2,-1.] by Th79,RFUNCT_2:61;
end;

theorem Th84:
  arccosec2 is_decreasing_on [.1,sqrt 2.]
proof
A1: [.1,sqrt 2.] = cosec.:[.PI/4,PI/2.] by Th44,RELAT_1:148;
    [.1,sqrt 2.] c= cosec.:].0,PI/2.] by A1,Lm12,RCOMP_2:19,RELAT_1:156;
    hence arccosec2 is_decreasing_on [.1,sqrt 2.] by Th80,RFUNCT_2:61;
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:84,XXREAL_1:128;then
A1: x in ].1,sqrt 2.[ or x in {1,sqrt 2} by XBOOLE_0:def 2;
    per cases by A1,TARSKI:def 2;
      suppose
      A2: x in ].1,sqrt 2.[;
      A3: 1 in [.1,sqrt 2.] by SQUARE_1:84,XXREAL_1:1;
      A4: [.1,sqrt 2.] /\ dom arcsec1 = [.1,sqrt 2.] by Th45,XBOOLE_1:28;
      A5: ].1,sqrt 2.[ c= [.1,sqrt 2.] by XXREAL_1:25;
          x in {s where s is Real: 1 < s & s < sqrt 2} by A2,RCOMP_1:def 2;then
      A6: ex s be Real st s=x & 1 < s & s < sqrt 2;then
      A7: 0 < arcsec1.x by A2,A3,A4,A5,Th73,Th81,RFUNCT_2:def 2;
          sqrt 2 in [.1,sqrt 2.] /\ dom arcsec1 by A4,SQUARE_1:84,XXREAL_1:1;
          then arcsec1.x < PI/4 by A2,A4,A5,A6,Th73,Th81,RFUNCT_2:def 2;
          hence arcsec1.x in [.0,PI/4.] by A7,XXREAL_1:1;
      end;
      suppose
      A8: x = 1;
          0 <= PI/4 by Lm9,XXREAL_1:3;
          hence arcsec1.x in [.0,PI/4.] by A8,Th73,XXREAL_1:1;
      end;
      suppose
      A9: x = sqrt 2;
          0 <= PI/4 by Lm9,XXREAL_1:3;
          hence arcsec1.x in [.0,PI/4.] by A9,Th73,XXREAL_1:1;
      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;
    assume
A1: x in [.-sqrt 2,-1.];
A2: -sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
    then x in ].-sqrt 2,-1.[ \/ {-sqrt 2,-1}
    by A1,XXREAL_1:128;then
A3: x in ].-sqrt 2,-1.[ or x in {-sqrt 2,-1} by XBOOLE_0:def 2;
    per cases by A3,TARSKI:def 2;
      suppose
      A4: x in ].-sqrt 2,-1.[;
      A5: -sqrt 2 in [.-sqrt 2,-1.] by A2,XXREAL_1:1;
      A6: [.-sqrt 2,-1.] /\ dom arcsec2 = [.-sqrt 2,-1.] by Th46,XBOOLE_1:28;
      A7: ].-sqrt 2,-1.[ c= [.-sqrt 2,-1.] by XXREAL_1:25;
          x in {s where s is Real: -sqrt 2 < s & s < -1}
          by A4,RCOMP_1:def 2;then
      A8: ex s be Real st s=x & -sqrt 2 < s & s < -1;then
      A9: 3/4*PI < arcsec2.x by A4,A5,A6,A7,Th74,Th82,RFUNCT_2:def 2;
          -1 in [.-sqrt 2,-1.] /\ dom arcsec2 by A2,A6,XXREAL_1:1;
          then arcsec2.x < PI by A4,A6,A7,A8,Th74,Th82,RFUNCT_2:def 2;
          hence arcsec2.x in [.3/4*PI,PI.] by A9,XXREAL_1:1;
      end;
      suppose
   A10: x = -sqrt 2;
        3/4*PI <= PI by Lm10,XXREAL_1:2;
        hence arcsec2.x in [.3/4*PI,PI.] by A10,Th74,XXREAL_1:1;
      end;
      suppose
   A11: x = -1;
        3/4*PI <= PI by Lm10,XXREAL_1:2;
        hence arcsec2.x in [.3/4*PI,PI.] by A11,Th74,XXREAL_1:1;
      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;
    assume
A1: x in [.-sqrt 2,-1.];
A2: -sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
    then x in ].-sqrt 2,-1.[ \/ {-sqrt 2,-1}
    by A1,XXREAL_1:128;then
A3: x in ].-sqrt 2,-1.[ or x in {-sqrt 2,-1} by XBOOLE_0:def 2;
    per cases by A3,TARSKI:def 2;
      suppose
      A4: x in ].-sqrt 2,-1.[;
      A5: -sqrt 2 in [.-sqrt 2,-1.] by A2,XXREAL_1:1;
      A6: [.-sqrt 2,-1.] /\ dom arccosec1 = [.-sqrt 2,-1.] by Th47,XBOOLE_1:28;
      A7: ].-sqrt 2,-1.[ c= [.-sqrt 2,-1.] by XXREAL_1:25;
          x in {s where s is Real: -sqrt 2 < s & s < -1}
          by A4,RCOMP_1:def 2;then
      A8: ex s be Real st s=x & -sqrt 2 < s & s < -1;then
      A9: -PI/4 > arccosec1.x by A4,A5,A6,A7,Th75,Th83,RFUNCT_2:def 3;
          -1 in [.-sqrt 2,-1.] /\ dom arccosec1 by A2,A6,XXREAL_1:1;
          then arccosec1.x > -PI/2 by A4,A6,A7,A8,Th75,Th83,RFUNCT_2:def 3;
          hence arccosec1.x in [.-PI/2,-PI/4.] by A9,XXREAL_1:1;
      end;
      suppose
      A10: x = -sqrt 2;
           -PI/2 <= -PI/4 by Lm11,XXREAL_1:3;
           hence arccosec1.x in [.-PI/2,-PI/4.] by A10,Th75,XXREAL_1:1;
      end;
      suppose
      A11: x = -1;
           -PI/2 <= -PI/4 by Lm11,XXREAL_1:3;
           hence arccosec1.x in [.-PI/2,-PI/4.] by A11,Th75,XXREAL_1:1;
      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:84,XXREAL_1:128;then
A1: x in ].1,sqrt 2.[ or x in {1,sqrt 2} by XBOOLE_0:def 2;
    per cases by A1,TARSKI:def 2;
      suppose
      A2: x in ].1,sqrt 2.[;
      A3: 1 in [.1,sqrt 2.] by SQUARE_1:84,XXREAL_1:1;
      A4: [.1,sqrt 2.] /\ dom arccosec2 = [.1,sqrt 2.] by Th48,XBOOLE_1:28;
      A5: ].1,sqrt 2.[ c= [.1,sqrt 2.] by XXREAL_1:25;
          x in {s where s is Real: 1 < s & s < sqrt 2} by A2,RCOMP_1:def 2;then
      A6: ex s be Real st s=x & 1 < s & s < sqrt 2;then
      A7: PI/2 > arccosec2.x by A2,A3,A4,A5,Th76,Th84,RFUNCT_2:def 3;
          sqrt 2 in [.1,sqrt 2.] /\ dom arccosec2 by A4,SQUARE_1:84,XXREAL_1:1;
          then arccosec2.x > PI/4 by A2,A4,A5,A6,Th76,Th84,RFUNCT_2:def 3;
          hence arccosec2.x in [.PI/4,PI/2.] by A7,XXREAL_1:1;
      end;
      suppose
      A8: x = 1;
          PI/4 <= PI/2 by Lm12,XXREAL_1:2;
          hence arccosec2.x in [.PI/4,PI/2.] by A8,Th76,XXREAL_1:1;
      end;
      suppose
      A9: x = sqrt 2;
          PI/4 <= PI/2 by Lm12,XXREAL_1:2;
          hence arccosec2.x in [.PI/4,PI/2.] by A9,Th76,XXREAL_1:1;
      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.] by XXREAL_1:1;then
A2: r in dom (arcsec1|[.1,sqrt 2.]) by Th45,RELAT_1:91;
    sec.(arcsec1 r)
    = ((sec|[.0,PI/4.]) qua Function).(arcsec1.r)
      by A1,Th85,FUNCT_1:72
   .= ((sec|[.0,PI/4.]) qua Function).((arcsec1|[.1,sqrt 2.]).r)
      by A1,FUNCT_1:72
   .= ((sec|[.0,PI/4.]) qua Function * (arcsec1|[.1,sqrt 2.])).r
      by A2,FUNCT_1:23
   .= (id [.1,sqrt 2.]).r by Th41,Th49,FUNCT_1:61
   .= r by A1,FUNCT_1:35;
    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.] by XXREAL_1:1;then
A2: r in dom (arcsec2|[.-sqrt 2,-1.]) by Th46,RELAT_1:91;
    sec.(arcsec2 r)
    = ((sec|[.3/4*PI,PI.]) qua Function).(arcsec2.r)
      by A1,Th86,FUNCT_1:72
   .= ((sec|[.3/4*PI,PI.]) qua Function).((arcsec2|[.-sqrt 2,-1.]).r)
      by A1,FUNCT_1:72
   .= ((sec|[.3/4*PI,PI.]) qua Function * (arcsec2|[.-sqrt 2,-1.])).r
      by A2,FUNCT_1:23
   .= (id [.-sqrt 2,-1.]).r by Th42,Th50,FUNCT_1:61
   .= r by A1,FUNCT_1:35;
    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.] by XXREAL_1:1;then
A2: r in dom (arccosec1|[.-sqrt 2,-1.]) by Th47,RELAT_1:91;
    cosec.(arccosec1 r)
    = ((cosec|[.-PI/2,-PI/4.]) qua Function).(arccosec1.r)
      by A1,Th87,FUNCT_1:72
   .= ((cosec|[.-PI/2,-PI/4.]) qua Function).((arccosec1|[.-sqrt 2,-1.]).r)
      by A1,FUNCT_1:72
   .= ((cosec|[.-PI/2,-PI/4.]) qua Function * (arccosec1|[.-sqrt 2,-1.])).r
      by A2,FUNCT_1:23
   .= (id [.-sqrt 2,-1.]).r by Th43,Th51,FUNCT_1:61
   .= r by A1,FUNCT_1:35;
    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.] by XXREAL_1:1;then
A2: r in dom (arccosec2|[.1,sqrt 2.]) by Th48,RELAT_1:91;
    cosec.(arccosec2 r)
    = ((cosec|[.PI/4,PI/2.]) qua Function).(arccosec2.r)
      by A1,Th88,FUNCT_1:72
   .= ((cosec|[.PI/4,PI/2.]) qua Function).((arccosec2|[.1,sqrt 2.]).r)
      by A1,FUNCT_1:72
   .= ((cosec|[.PI/4,PI/2.]) qua Function * (arccosec2|[.1,sqrt 2.])).r
      by A2,FUNCT_1:23
   .= (id [.1,sqrt 2.]).r by Th44,Th52,FUNCT_1:61
   .= r by A1,FUNCT_1:35;
    hence thesis;
end;

theorem Th93:
  arcsec1 is_continuous_on [.1,sqrt 2.]
proof
    set f = sec | [.0,PI/4.];
A1: f|[.0,PI/4.] = f by RELAT_1:101;
    0 <= PI/4 by Lm9,XXREAL_1:3;then
    (f|[.0,PI/4.])" is_continuous_on f.:[.0,PI/4.]
    by Lm13,Lm21,FCONT_1:54;
    then arcsec1|[.1,sqrt 2.] is_continuous_on [.1,sqrt 2.]
    by A1,Th41,Th49,RELAT_1:148;
    hence arcsec1 is_continuous_on [.1,sqrt 2.] by FCONT_1:16;
end;

theorem Th94:
  arcsec2 is_continuous_on [.-sqrt 2,-1.]
proof
    set f = sec | [.3/4*PI,PI.];
A1: f|[.3/4*PI,PI.] = f by RELAT_1:101;
    3/4*PI <= PI by Lm10,XXREAL_1:2;then
    (f|[.3/4*PI,PI.])" is_continuous_on f.:[.3/4*PI,PI.]
    by Lm14,Lm22,FCONT_1:54;
    then arcsec2|[.-sqrt 2,-1.] is_continuous_on [.-sqrt 2,-1.]
    by A1,Th42,Th50,RELAT_1:148;
    hence arcsec2 is_continuous_on [.-sqrt 2,-1.] by FCONT_1:16;
end;

theorem Th95:
  arccosec1 is_continuous_on [.-sqrt 2,-1.]
proof
    set f = cosec | [.-PI/2,-PI/4.];
A1: f|[.-PI/2,-PI/4.] = f by RELAT_1:101;
    -PI/2 <= -PI/4 by Lm11,XXREAL_1:3;then
    (f|[.-PI/2,-PI/4.])" is_continuous_on f.:[.-PI/2,-PI/4.]
    by Lm15,Lm23,FCONT_1:54;
    then arccosec1|[.-sqrt 2,-1.] is_continuous_on [.-sqrt 2,-1.]
    by A1,Th43,Th51,RELAT_1:148;
    hence arccosec1 is_continuous_on [.-sqrt 2,-1.] by FCONT_1:16;
end;

theorem Th96:
  arccosec2 is_continuous_on [.1,sqrt 2.]
proof
    set f = cosec | [.PI/4,PI/2.];
A1: f|[.PI/4,PI/2.] = f by RELAT_1:101;
    PI/4 <= PI/2 by Lm12,XXREAL_1:2;then
    (f|[.PI/4,PI/2.])" is_continuous_on f.:[.PI/4,PI/2.]
    by Lm16,Lm24,FCONT_1:54;
    then arccosec2|[.1,sqrt 2.] is_continuous_on [.1,sqrt 2.]
    by A1,Th44,Th52,RELAT_1:148;
    hence arccosec2 is_continuous_on [.1,sqrt 2.] by FCONT_1:16;
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 2;
        then consider x be Real such that
    A2: x in [.1,sqrt 2.] and
    A3: y1 = arcsec1.x by Th93,SQUARE_1:84,FCONT_2:16;
        take x;
        thus x in dom (arcsec1 | [.1,sqrt 2.]) &
        y = (arcsec1 | [.1,sqrt 2.]).x
        by A2,A3,Th45,RELAT_1:91,FUNCT_1:72;
    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
    A4: x in dom (arcsec1 | [.1,sqrt 2.]) and
    A5: y = (arcsec1 | [.1,sqrt 2.]).x;
    A6: dom (arcsec1 | [.1,sqrt 2.]) = [.1,sqrt 2.] by Th45,RELAT_1:91;
        reconsider x1=x as Real by A4;
        y = arcsec1.x by A4,A5,A6,FUNCT_1:72;
        hence y in [.0,PI/4.] by A4,A6,Th85;
    end;
  end;
  hence thesis by FUNCT_1:def 5;
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;
    A2: -sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
        y1 in [.arcsec2.(-sqrt 2),arcsec2.(-1).] \/
        [.arcsec2.(-1),arcsec2.(-sqrt 2).] by A1,Th74,XBOOLE_0:def 2;
        then consider x be Real such that
    A3: x in [.-sqrt 2,-1.] and
    A4: y1 = arcsec2.x by A2,Th94,FCONT_2:16;
        take x;
        thus x in dom (arcsec2 | [.-sqrt 2,-1.]) &
        y = (arcsec2 | [.-sqrt 2,-1.]).x
        by A3,A4,Th46,RELAT_1:91,FUNCT_1:72;
    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
    A5: x in dom (arcsec2 | [.-sqrt 2,-1.]) and
    A6: y = (arcsec2 | [.-sqrt 2,-1.]).x;
    A7: dom (arcsec2 | [.-sqrt 2,-1.]) = [.-sqrt 2,-1.] by Th46,RELAT_1:91;
        reconsider x1=x as Real by A5;
        y = arcsec2.x by A5,A6,A7,FUNCT_1:72;
        hence y in [.3/4*PI,PI.] by A5,A7,Th86;
    end;
  end;
  hence thesis by FUNCT_1:def 5;
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;
    A2: -sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
        y1 in [.arccosec1.(-1),arccosec1.(-sqrt 2).] \/
        [.arccosec1.(-sqrt 2),arccosec1.(-1).] by A1,Th75,XBOOLE_0:def 2;
        then consider x be Real such that
    A3: x in [.-sqrt 2,-1.] and
    A4: y1 = arccosec1.x by A2,Th95,FCONT_2:16;
        take x;
        thus x in dom (arccosec1 | [.-sqrt 2,-1.]) &
        y = (arccosec1 | [.-sqrt 2,-1.]).x
        by A3,A4,Th47,RELAT_1:91,FUNCT_1:72;
    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
  A5: x in dom (arccosec1 | [.-sqrt 2,-1.]) and
  A6: y = (arccosec1 | [.-sqrt 2,-1.]).x;
  A7: dom (arccosec1 | [.-sqrt 2,-1.]) = [.-sqrt 2,-1.] by Th47,RELAT_1:91;
      reconsider x1=x as Real by A5;
      y = arccosec1.x by A5,A6,A7,FUNCT_1:72;
      hence y in [.-PI/2,-PI/4.] by A5,A7,Th87;
    end;
  end;
  hence thesis by FUNCT_1:def 5;
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 2;
        then consider x be Real such that
    A2: x in [.1,sqrt 2.] and
    A3: y1 = arccosec2.x by Th96,SQUARE_1:84,FCONT_2:16;
        take x;
        thus x in dom (arccosec2 | [.1,sqrt 2.]) &
        y = (arccosec2 | [.1,sqrt 2.]).x
        by A2,A3,Th48,RELAT_1:91,FUNCT_1:72;
    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
    A4: x in dom (arccosec2 | [.1,sqrt 2.]) and
    A5: y = (arccosec2 | [.1,sqrt 2.]).x;
    A6: dom (arccosec2 | [.1,sqrt 2.]) = [.1,sqrt 2.] by Th48,RELAT_1:91;
        reconsider x1=x as Real by A4;
        y = arccosec2.x by A4,A5,A6,FUNCT_1:72;
        hence y in [.PI/4,PI/2.] by A4,A6,Th88;
    end;
  end;
  hence thesis by FUNCT_1:def 5;
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.] by XXREAL_1:1;
    then r in dom (arcsec1 | [.1,sqrt 2.]) by Th45,RELAT_1:91;
    then (arcsec1 | [.1,sqrt 2.]).r in rng(arcsec1 | [.1,sqrt 2.])
    by FUNCT_1:def 5;
    then arcsec1 r in rng(arcsec1 | [.1,sqrt 2.]) by A1,FUNCT_1:72;
    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.] by XXREAL_1:1;
    then r in dom (arcsec2 | [.-sqrt 2,-1.]) by Th46,RELAT_1:91;
    then (arcsec2 | [.-sqrt 2,-1.]).r in rng(arcsec2 | [.-sqrt 2,-1.])
    by FUNCT_1:def 5;
    then arcsec2 r in rng(arcsec2 | [.-sqrt 2,-1.]) by A1,FUNCT_1:72;
    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.] by XXREAL_1:1;
    then r in dom (arccosec1 | [.-sqrt 2,-1.]) by Th47,RELAT_1:91;
    then (arccosec1 | [.-sqrt 2,-1.]).r in rng(arccosec1 | [.-sqrt 2,-1.])
    by FUNCT_1:def 5;
    then arccosec1 r in rng(arccosec1 | [.-sqrt 2,-1.]) by A1,FUNCT_1:72;
    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.] by XXREAL_1:1;
    then r in dom (arccosec2 | [.1,sqrt 2.]) by Th48,RELAT_1:91;
    then (arccosec2 | [.1,sqrt 2.]).r in rng(arccosec2 | [.1,sqrt 2.])
    by FUNCT_1:def 5;
    then arccosec2 r in rng(arccosec2 | [.1,sqrt 2.]) by A1,FUNCT_1:72;
    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 0 <= arcsec1 r & arcsec1 r <= PI/4 by Th105;
    then 0 < arcsec1 r & arcsec1 r < PI/4 or
    0 = arcsec1 r or arcsec1 r = PI/4 by REAL_1:def 5;
    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 REAL_1:def 5;
    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 REAL_1:def 5;
    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 REAL_1:def 5;
    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
A1:  1 <= r & r <= sqrt 2;then
     r in [.1,sqrt 2.] by XXREAL_1:1;then
A2:  x in dom (sec | [.0,PI/4.]) by Lm13,Th85;
A3:  dom (sec | [.0,PI/4.]) c= dom sec by RELAT_1:89;
A5:  r = (cos^).x by A1,Th89
     .= 1/cos.x by A2,A3,RFUNCT_1:def 8;
     r > 0 by A1,XXREAL_0:2;then
A7:  r^2 > 0 by SQUARE_1:74;
     (sin.x)^2+(cos.x)^2 = 1 by SIN_COS:31;then
A8:  (sin.x)^2 = 1-(cos.x)^2
     .= 1-(1/r)*(1/r) by A5
     .= 1-1/(r^2) by XCMPLX_1:103
     .= (r^2)/(r^2)-1/(r^2) by A7,XCMPLX_1:60
     .= (r^2-1)/(r^2);
     r^2 >= 1^2 by A1,SQUARE_1:77;then
A9:  r^2-1 >= 0 by XREAL_1:50;then
A10: (r^2-1)/(r^2) >= 0 by A7,XREAL_1:138;
A12: 0 in [.0,PI.] by COMPTRIG:21,XXREAL_1:1;
A13: PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;
     PI/4 < PI/1 by COMPTRIG:21,REAL_2:200;
     then PI/4 in [.0,PI.] by A13,XXREAL_1:1;
     then [.0,PI/4.] c= [.0,PI.] by A12,RCOMP_1:16;
     then sin.x >= 0 by A2,Lm13,COMPTRIG:24;
     then sin.x = sqrt ((r^2-1)/(r^2)) by A8,A10,SQUARE_1:def 4
     .= sqrt(r^2-1)/sqrt(r^2) by A7,A9,SQUARE_1:99
     .= sqrt(r^2-1)/r by A1,XXREAL_0:2,SQUARE_1:89;
     hence thesis by A5;
end;

theorem Th114:
  -sqrt 2 <= r & r <= -1 implies sin.(arcsec2 r) = -sqrt(r^2-1)/r &
  cos.(arcsec2 r) = 1/r
proof
     set x = arcsec2 r;
     assume
A1:  -sqrt 2 <= r & r <= -1;then
     r in [.-sqrt 2,-1.] by XXREAL_1:1;then
A2:  x in dom (sec | [.3/4*PI,PI.]) by Lm14,Th86;
A3:  dom (sec | [.3/4*PI,PI.]) c= dom sec by RELAT_1:89;
A5:  r = (cos^).x by A1,Th90
     .= 1/cos.x by A2,A3,RFUNCT_1:def 8;
     r < 0 by A1,XXREAL_0:2;then
A7:  r^2 > 0 by SQUARE_1:74;
     (sin.x)^2+(cos.x)^2 = 1 by SIN_COS:31;then
A8:  (sin.x)^2 = 1-(cos.x)^2
     .= 1-(1/r)*(1/r) by A5
     .= 1-1/(r^2) by XCMPLX_1:103
     .= (r^2)/(r^2)-1/(r^2) by A7,XCMPLX_1:60
     .= (r^2-1)/(r^2);
     -r >= -(-1) by A1,XREAL_1:26;
     then (-r)^2 >= 1^2 by SQUARE_1:77;then
A9:  r^2-1 >= 0 by XREAL_1:50;then
A10: (r^2-1)/(r^2) >= 0 by A7,XREAL_1:138;
     3/4*PI > PI/2 by Lm10,XXREAL_1:2;then
A11: 3/4*PI > 0 by COMPTRIG:21,XXREAL_0:2;
     3/4*PI <= PI by Lm10,XXREAL_1:2;then
A12: 3/4*PI in [.0,PI.] by A11,XXREAL_1:1;
     PI in [.0,PI.] by COMPTRIG:21,XXREAL_1:1;
     then [.3/4*PI,PI.] c= [.0,PI.] by A12,RCOMP_1:16;
     then sin.x >= 0 by A2,Lm14,COMPTRIG:24;
     then sin.x = sqrt ((r^2-1)/(r^2)) by A8,A10,SQUARE_1:def 4
     .= sqrt(r^2-1)/sqrt(r^2) by A7,A9,SQUARE_1:99
     .= sqrt(r^2-1)/(-r) by A1,XXREAL_0:2,SQUARE_1:90
     .= -sqrt(r^2-1)/r by XCMPLX_1:189;
     hence thesis by A5;
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
A1:  -sqrt 2 <= r & r <= -1;
     then r in [.-sqrt 2,-1.] by XXREAL_1:1;then
A2:  x in dom (cosec | [.-PI/2,-PI/4.]) by Lm15,Th87;
A3:  dom (cosec | [.-PI/2,-PI/4.]) c= dom cosec by RELAT_1:89;
A8:  r = (sin^).x by A1,Th91
     .= 1/sin.x by A2,A3,RFUNCT_1:def 8;
     r < 0 by A1,XXREAL_0:2;then
A10: r^2 > 0 by SQUARE_1:74;
     (sin.x)^2+(cos.x)^2 = 1 by SIN_COS:31;then
A11: (cos.x)^2 = 1-(sin.x)^2
     .= 1-(1/r)*(1/r) by A8
     .= 1-1/(r^2) by XCMPLX_1:103
     .= (r^2)/(r^2)-1/(r^2) by A10,XCMPLX_1:60
     .= (r^2-1)/(r^2);
     -r >= -(-1) by A1,XREAL_1:26;
     then (-r)^2 >= 1^2 by SQUARE_1:77;then
A12: r^2-1 >= 0 by XREAL_1:50;then
A13: (r^2-1)/(r^2) >= 0 by A10,XREAL_1:138;
A14: -PI/2 in [.-PI/2,PI/2.] by XXREAL_1:1;
A15: -PI/4 >= -PI/2 & -PI/4 < 0 by Lm11,XXREAL_1:3;
     -PI/4 in [.-PI/2,PI/2.] by A15,XXREAL_1:1;
     then [.-PI/2,-PI/4.] c= [.-PI/2,PI/2.] by A14,RCOMP_1:16;
     then cos.x >= 0 by A2,Lm15,COMPTRIG:28;
     then cos.x = sqrt ((r^2-1)/(r^2)) by A11,A13,SQUARE_1:def 4
     .= sqrt(r^2-1)/sqrt(r^2) by A10,A12,SQUARE_1:99
     .= sqrt(r^2-1)/(-r) by A1,XXREAL_0:2,SQUARE_1:90
     .= -sqrt(r^2-1)/r by XCMPLX_1:189;
     hence thesis by A8;
end;

theorem Th116:
  1 <= r & r <= sqrt 2 implies sin.(arccosec2 r) = 1/r &
  cos.(arccosec2 r) = sqrt(r^2-1)/r
proof
     set x = arccosec2 r;
     assume
A1:  1 <= r & r <= sqrt 2;then
     r in [.1,sqrt 2.] by XXREAL_1:1;then
A2:  x in dom (cosec | [.PI/4,PI/2.]) by Lm16,Th88;
A3:  dom (cosec | [.PI/4,PI/2.]) c= dom cosec by RELAT_1:89;
A5:  r = (sin^).x by A1,Th92
     .= 1/sin.x by A2,A3,RFUNCT_1:def 8;
     r > 0 by A1,XXREAL_0:2;then
A7:  r^2 > 0 by SQUARE_1:74;
     (sin.x)^2+(cos.x)^2 = 1 by SIN_COS:31;then
A8:  (cos.x)^2 = 1-(sin.x)^2
     .= 1-(1/r)*(1/r) by A5
     .= 1-1/(r^2) by XCMPLX_1:103
     .= (r^2)/(r^2)-1/(r^2) by A7,XCMPLX_1:60
     .= (r^2-1)/(r^2);
     r^2 >= 1^2 by A1,SQUARE_1:77;then
A9:  r^2-1 >= 0 by XREAL_1:50;then
A10: (r^2-1)/(r^2) >= 0 by A7,XREAL_1:138;
A11: PI/4 <= PI/2 by Lm12,XXREAL_1:2;
A12: PI/4 in [.-PI/2,PI/2.] by A11,XXREAL_1:1;
     PI/2 in [.-PI/2,PI/2.] by XXREAL_1:1;
     then [.PI/4,PI/2.] c= [.-PI/2,PI/2.] by A12,RCOMP_1:16;
     then cos.x >= 0 by A2,Lm16,COMPTRIG:28;
     then cos.x = sqrt ((r^2-1)/(r^2)) by A8,A10,SQUARE_1:def 4
     .= sqrt(r^2-1)/sqrt(r^2) by A7,A9,SQUARE_1:99
     .= sqrt(r^2-1)/r by A1,XXREAL_0:2,SQUARE_1:89;
     hence thesis by A5;
end;

theorem
  1 < r & r < sqrt 2 implies cosec.(arcsec1 r) = r/sqrt(r^2-1)
proof
    set x = arcsec1 r;
    assume
A1: 1 < r & r < sqrt 2;
    then 0 < arcsec1 r & arcsec1 r < PI/4 by Th109;then
A2: x in ].0,PI/4.[ by XXREAL_1:4;
    PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;then
A3: ].0,PI/4.[ c= ].0,PI/2.[ by XXREAL_1:46;
    ].0,PI/2.] = ].0,PI/2.[ \/ {PI/2} by COMPTRIG:21,XXREAL_1:132;
    then ].0,PI/2.[ c= ].0,PI/2.] by XBOOLE_1:7;
    then ].0,PI/4.[ c= ].0,PI/2.] by A3,XBOOLE_1:1;then
A4: ].0,PI/4.[ c= dom cosec by Th4,XBOOLE_1:1;
    cosec.x = 1/sin.x by A2,A4,RFUNCT_1:def 8
    .= 1/(sqrt(r^2-1)/r) by A1,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;
    assume
A1: -sqrt 2 < r & r < -1;
    then 3/4*PI < arcsec2 r & arcsec2 r < PI by Th110;then
A2: x in ].3/4*PI,PI.[ by XXREAL_1:4;
AA: ].3/4*PI,PI.[ c= dom cosec
    proof
        set f = sin^;
    A3: ].3/4*PI,PI.[ \ sin"{0} c= dom sin \ sin"{0} by SIN_COS:27,XBOOLE_1:33;
        ].3/4*PI,PI.[ /\ sin"{0} = {}
        proof
            assume ].3/4*PI,PI.[ /\ sin"{0} <> {};
            then consider rr such that
        A4: rr in ].3/4*PI,PI.[ /\ sin"{0} by XBOOLE_0:def 1;
        A5: rr in ].3/4*PI,PI.[ & rr in sin"{0} by A4,XBOOLE_0:def 3;
            3/4*PI >= 3/4*0 by COMPTRIG:21,XREAL_1:66;
            then ].3/4*PI,PI.[ c= ].0,PI.[ by XXREAL_1:46;then
        A7: sin.rr <> 0 by A5,COMPTRIG:23;
            sin.rr in {0} by A5,FUNCT_1:def 13;
        hence contradiction by A7,TARSKI:def 1;
        end;
        then ].3/4*PI,PI.[ misses sin"{0} by XBOOLE_0:def 7;
        then ].3/4*PI,PI.[ c= dom sin \ sin"{0} by A3,XBOOLE_1:83;
        hence ].3/4*PI,PI.[ c= dom cosec by RFUNCT_1:def 8;
    end;
    cosec.x = 1/sin.x by A2,AA,RFUNCT_1:def 8
    .= 1/(-sqrt(r^2-1)/r) by A1,Th114
    .= -1/(sqrt(r^2-1)/r) by XCMPLX_1:189
    .= -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;
    assume
A1: -sqrt 2 < r & r < -1;
    then -PI/2 < arccosec1 r & arccosec1 r < -PI/4 by Th111;then
A2: x in ].-PI/2,-PI/4.[ by XXREAL_1:4;
AA: ].-PI/2,-PI/4.[ c= dom sec
    proof
        set f = cos^;
    A3: ].-PI/2,-PI/4.[ \ cos"{0} c= dom cos \ cos"{0}
        by SIN_COS:27,XBOOLE_1:33;
        ].-PI/2,-PI/4.[ /\ cos"{0} = {}
        proof
            assume ].-PI/2,-PI/4.[ /\ cos"{0} <> {};
            then consider rr such that
        A4: rr in ].-PI/2,-PI/4.[ /\ cos"{0} by XBOOLE_0:def 1;
        A5: rr in ].-PI/2,-PI/4.[ & rr in cos"{0} by A4,XBOOLE_0:def 3;
            ].-PI/2,-PI/4.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;then
        A7: cos.rr <> 0 by A5,COMPTRIG:27;
            cos.rr in {0} by A5,FUNCT_1:def 13;
            hence contradiction by A7,TARSKI:def 1;
        end;
        then ].-PI/2,-PI/4.[ misses cos"{0} by XBOOLE_0:def 7;
        then ].-PI/2,-PI/4.[ c= dom cos \ cos"{0} by A3,XBOOLE_1:83;
        hence ].-PI/2,-PI/4.[ c= dom sec by RFUNCT_1:def 8;
    end;
    sec.x = 1/cos.x by A2,AA,RFUNCT_1:def 8
    .= 1/(-sqrt(r^2-1)/r) by A1,Th115
    .= -1/(sqrt(r^2-1)/r) by XCMPLX_1:189
    .= -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;
    assume
A1: 1 < r & r < sqrt 2;
    then PI/4 < arccosec2 r & arccosec2 r < PI/2 by Th112;then
A2: x in ].PI/4,PI/2.[ by XXREAL_1:4;
    PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;then
A3: ].PI/4,PI/2.[ c= ].0,PI/2.[ by XXREAL_1:46;
    [.0,PI/2.[ = ].0,PI/2.[ \/ {0} by COMPTRIG:21,XXREAL_1:131;
    then ].0,PI/2.[ c= [.0,PI/2.[ by XBOOLE_1:7;
    then ].PI/4,PI/2.[ c= [.0,PI/2.[ by A3,XBOOLE_1:1;then
A4: ].PI/4,PI/2.[ c= dom sec by Th1,XBOOLE_1:1;
    sec.x = 1/cos.x by A2,A4,RFUNCT_1:def 8
    .= 1/(sqrt(r^2-1)/r) by A1,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 f = sec|[.0,PI/2.[;
     set g = f|].0,PI/2.[;
     set g1 = arcsec1|(sec.:].0,PI/2.[);
     set X = sec.:].0,PI/2.[;
A0:  ].0,PI/2.[ c= [.0,PI/2.[ by XXREAL_1:22;then
A1:  g = sec|].0,PI/2.[ by RELAT_1:103;
A2:  dom ((g|].0,PI/2.[)") = rng (g|].0,PI/2.[) by FUNCT_1:55
     .= rng(sec|].0,PI/2.[) by A1,RELAT_1:101
     .= sec.:].0,PI/2.[ by RELAT_1:148;
A3:  g is_differentiable_on ].0,PI/2.[ by A1,Th5,FDIFF_2:16;
AA:  now
         let x0 be Real such that
     A4: x0 in ].0,PI/2.[;
     A5: diff(g,x0) = (g`|].0,PI/2.[).x0 by A3,A4,FDIFF_1:def 8
                   .= ((sec|].0,PI/2.[)`|].0,PI/2.[).x0 by A0,RELAT_1:103
                   .= (sec`|].0,PI/2.[).x0 by Th5,FDIFF_2:16
                   .= diff(sec,x0) by A4,Th5,FDIFF_1:def 8
                   .= sin.x0/(cos.x0)^2 by A4,Th5;
         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= ].0,PI.[ by COMPTRIG:21,XXREAL_1:46;then
         A7: sin.x0 > 0 by A6,COMPTRIG:23;
             ].0,PI/2.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,XXREAL_1:46;
             then cos.x0 > 0 by A6,COMPTRIG:27;
             then (cos.x0)^2 > 0 by SQUARE_1:74;
             then sin.x0/(cos.x0)^2 > 0/(cos.x0)^2 by A7,REAL_1:73;
             hence sin.x0/(cos.x0)^2 > 0;
         end;
         hence diff(g,x0) > 0 by A4,A5;
     end;
AB:  (g|].0,PI/2.[)" = (f|].0,PI/2.[)" by RELAT_1:101
     .= arcsec1|(f.:].0,PI/2.[) by RFUNCT_2:40
     .= arcsec1|(rng(f|].0,PI/2.[)) by RELAT_1:148
     .= arcsec1|(rng (sec|].0,PI/2.[)) by A0,RELAT_1:103
     .= arcsec1|(sec.:].0,PI/2.[) by RELAT_1:148;then
A9:  g1 is_differentiable_on X by A2,A3,AA,FDIFF_2:48;
A11: X c= dom arcsec1 by A2,AB,RELAT_1:89;
     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 7;
       hence arcsec1|X is_differentiable_in x by RELAT_1:101;
     end;
     hence arcsec1 is_differentiable_on sec.:].0,PI/2.[ by A11,FDIFF_1:def 7;
end;

theorem Th122:
  arcsec2 is_differentiable_on sec.:].PI/2,PI.[
proof
     set f = sec|].PI/2,PI.];
     set g = f|].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:  g = sec|].PI/2,PI.[ by RELAT_1:103;
A2:  dom ((g|].PI/2,PI.[)") = rng (g|].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:  g is_differentiable_on ].PI/2,PI.[ by A1,Th6,FDIFF_2:16;
AA:  now
       let x0 be Real such that
   A4: x0 in ].PI/2,PI.[;
   A5: diff(g,x0) = (g`|].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 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= ].0,PI.[ by COMPTRIG:21,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 by SQUARE_1:74;
         then sin.x0/(cos.x0)^2 > 0/(cos.x0)^2 by A7,REAL_1:73;
         hence sin.x0/(cos.x0)^2 > 0;
       end;
       hence diff(g,x0) > 0 by A4,A5;
     end;
AB:  (g|].PI/2,PI.[)" = (f|].PI/2,PI.[)" by RELAT_1:101
     .= arcsec2|(f.:].PI/2,PI.[) by RFUNCT_2:40
     .= arcsec2|(rng(f|].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:  g1 is_differentiable_on X by A2,A3,AA,FDIFF_2:48;
A11: X c= dom arcsec2 by A2,AB,RELAT_1:89;
     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 7;
       hence arcsec2|X is_differentiable_in x by RELAT_1:101;
     end;
     hence arcsec2 is_differentiable_on sec.:].PI/2,PI.[
     by A11,FDIFF_1:def 7;
end;

theorem Th123:
  arccosec1 is_differentiable_on cosec.:].-PI/2,0.[
proof
     set f = cosec|[.-PI/2,0.[;
     set g = f|].-PI/2,0.[;
     set g1 = arccosec1|(cosec.:].-PI/2,0.[);
     set X = cosec.:].-PI/2,0.[;
A0:  ].-PI/2,0.[ c= [.-PI/2,0.[ by XXREAL_1:22;then
A1:  g = cosec|].-PI/2,0.[ by RELAT_1:103;
A2:  dom ((g|].-PI/2,0.[)") = rng (g|].-PI/2,0.[) by FUNCT_1:55
     .= rng(cosec|].-PI/2,0.[) by A1,RELAT_1:101
     .= cosec.:].-PI/2,0.[ by RELAT_1:148;
A3:  g is_differentiable_on ].-PI/2,0.[ by A1,Th7,FDIFF_2:16;
AA:  now
       let x0 be Real such that
   A4: x0 in ].-PI/2,0.[;
   A5: diff(g,x0) = (g`|].-PI/2,0.[).x0 by A3,A4,FDIFF_1:def 8
                 .= ((cosec|].-PI/2,0.[)`|].-PI/2,0.[).x0
                  by A0,RELAT_1:103
                 .= (cosec`|].-PI/2,0.[).x0 by Th7,FDIFF_2:16
                 .= diff(cosec,x0) by A4,Th7,FDIFF_1:def 8
                 .= -cos.x0/(sin.x0)^2 by A4,Th7;
       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.[;
         ].-PI/2,0.[ \/ {-PI/2} = [.-PI/2,0.[ by COMPTRIG:21,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 & x0 < 0 by A6,XXREAL_1:4;
         then -PI+2*PI < x0+2*PI & x0+2*PI < 0+2*PI by XREAL_1:10;
         then x0+2*PI in ].PI,2*PI.[ by XXREAL_1:4;
         then sin.(x0+2*PI) < 0 by COMPTRIG:25;
         then sin.x0 < 0 by SIN_COS:83;then
     A7: (sin.x0)^2 > 0 by SQUARE_1:74;
         ].-PI/2,0.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,XXREAL_1:46;
         then cos.x0 > 0 by A6,COMPTRIG:27;
         then cos.x0/(sin.x0)^2 > 0/(sin.x0)^2 by A7,REAL_1:73;
         then -(cos.x0/(sin.x0)^2) < -0 by XREAL_1:26;
         hence -cos.x0/(sin.x0)^2 < 0;
       end;
       hence diff(g,x0) < 0 by A4,A5;
     end;
AB:  (g|].-PI/2,0.[)" = (f|].-PI/2,0.[)" by RELAT_1:101
     .= arccosec1|(f.:].-PI/2,0.[) by RFUNCT_2:40
     .= arccosec1|(rng(f|].-PI/2,0.[)) by RELAT_1:148
     .= arccosec1|(rng (cosec|].-PI/2,0.[)) by A0,RELAT_1:103
     .= arccosec1|(cosec.:].-PI/2,0.[) by RELAT_1:148;then
A9:  g1 is_differentiable_on X by A2,A3,AA,FDIFF_2:48;
A11: X c= dom arccosec1 by A2,AB,RELAT_1:89;
     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 A9,FDIFF_1:def 7;
       hence arccosec1|X is_differentiable_in x by RELAT_1:101;
     end;
     hence arccosec1 is_differentiable_on cosec.:].-PI/2,0.[
     by A11,FDIFF_1:def 7;
end;

theorem Th124:
  arccosec2 is_differentiable_on cosec.:].0,PI/2.[
proof
     set f = cosec|].0,PI/2.];
     set g = f|].0,PI/2.[;
     set g1 = arccosec2|(cosec.:].0,PI/2.[);
     set X = cosec.:].0,PI/2.[;
A0:  ].0,PI/2.[ c= ].0,PI/2.] by XXREAL_1:21;then
A1:  g = cosec|].0,PI/2.[ by RELAT_1:103;
A2:  dom ((g|].0,PI/2.[)") = rng (g|].0,PI/2.[) by FUNCT_1:55
     .= rng(cosec|].0,PI/2.[) by A1,RELAT_1:101
     .= cosec.:].0,PI/2.[ by RELAT_1:148;
A3:  g is_differentiable_on ].0,PI/2.[ by A1,Th8,FDIFF_2:16;
AA:  now
       let x0 be Real such that
   A4: x0 in ].0,PI/2.[;
   A5: diff(g,x0) = (g`|].0,PI/2.[).x0 by A3,A4,FDIFF_1:def 8
                 .= ((cosec|].0,PI/2.[)`|].0,PI/2.[).x0 by A0,RELAT_1:103
                 .= (cosec`|].0,PI/2.[).x0 by Th8,FDIFF_2:16
                 .= diff(cosec,x0) by A4,Th8,FDIFF_1:def 8
                 .= -cos.x0/(sin.x0)^2 by A4,Th8;
       for x0 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= ].0,PI.[ by COMPTRIG:21,XXREAL_1:46;
         then sin.x0 > 0 by A6,COMPTRIG:23;then
     A7: (sin.x0)^2 > 0 by SQUARE_1:74;
         ].0,PI/2.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,XXREAL_1:46;
         then cos.x0 > 0 by A6,COMPTRIG:27;
         then cos.x0/(sin.x0)^2 > 0/(sin.x0)^2 by A7,REAL_1:73;
         then -(cos.x0/(sin.x0)^2) < -0 by XREAL_1:26;
         hence -cos.x0/(sin.x0)^2 < 0;
       end;
       hence diff(g,x0) < 0 by A4,A5;
     end;
AB:  (g|].0,PI/2.[)" = (f|].0,PI/2.[)" by RELAT_1:101
     .= arccosec2|(f.:].0,PI/2.[) by RFUNCT_2:40
     .= arccosec2|(rng(f|].0,PI/2.[)) by RELAT_1:148
     .= arccosec2|(rng (cosec|].0,PI/2.[)) by A0,RELAT_1:103
     .= arccosec2|(cosec.:].0,PI/2.[) by RELAT_1:148;then
A9:  g1 is_differentiable_on X by A2,A3,AA,FDIFF_2:48;
A11: X c= dom arccosec2 by A2,AB,RELAT_1:89;
     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 7;
       hence arccosec2|X is_differentiable_in x by RELAT_1:101;
     end;
     hence arccosec2 is_differentiable_on cosec.:].0,PI/2.[
     by A11,FDIFF_1:def 7;
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= ].0,PI.[ by COMPTRIG:21,XXREAL_1:46;then
A2: sin.x0 > 0 by A1,COMPTRIG:23;
    ].0,PI/2.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,XXREAL_1:46;
    then cos.x0 > 0 by A1,COMPTRIG:27;
    then (cos.x0)^2 > 0 by SQUARE_1:74;
    then sin.x0/(cos.x0)^2 > 0/(cos.x0)^2 by A2,REAL_1:73;
    hence diff(sec,x0) > 0 by A1,Th5;
  end;
  then rng(sec|].0,PI/2.[) is open by Th5,FDIFF_2:41;
  hence sec.:].0,PI/2.[ is open by RELAT_1:148;
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= ].0,PI.[ by COMPTRIG:21,XXREAL_1:46;then
A2: sin.x0 > 0 by A1,COMPTRIG:23;
    ].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by COMPTRIG:21,XXREAL_1:46;
    then cos.x0 < 0 by A1,COMPTRIG:29;
    then (cos.x0)^2 > 0 by SQUARE_1:74;
    then sin.x0/(cos.x0)^2 > 0/(cos.x0)^2 by A2,REAL_1:73;
    hence diff(sec,x0) > 0 by A1,Th6;
  end;
  then rng(sec|].PI/2,PI.[) is open by Th6,FDIFF_2:41;
  hence sec.:].PI/2,PI.[ is open by RELAT_1:148;
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.[;
    ].-PI/2,0.[ \/ {-PI/2} = [.-PI/2,0.[ by COMPTRIG:21,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 & x0 < 0 by A1,XXREAL_1:4;
    then -PI+2*PI < x0+2*PI & x0+2*PI < 0+2*PI by XREAL_1:10;
    then x0+2*PI in ].PI,2*PI.[ by XXREAL_1:4;
    then sin.(x0+2*PI) < 0 by COMPTRIG:25;
    then sin.x0 < 0 by SIN_COS:83;then
A2: (sin.x0)^2 > 0 by SQUARE_1:74;
    ].-PI/2,0.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,XXREAL_1:46;
    then cos.x0 > 0 by A1,COMPTRIG:27;
    then cos.x0/(sin.x0)^2 > 0/(sin.x0)^2 by A2,REAL_1:73;
    then -(cos.x0/(sin.x0)^2) < -0 by XREAL_1:26;
    hence diff(cosec,x0) < 0 by A1,Th7;
  end;
  then rng(cosec|].-PI/2,0.[) is open by Th7,FDIFF_2:41;
  hence cosec.:].-PI/2,0.[ is open by RELAT_1:148;
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= ].0,PI.[ by COMPTRIG:21,XXREAL_1:46;
    then sin.x0 > 0 by A1,COMPTRIG:23;then
A2: (sin.x0)^2 > 0 by SQUARE_1:74;
    ].0,PI/2.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,XXREAL_1:46;
    then cos.x0 > 0 by A1,COMPTRIG:27;
    then cos.x0/(sin.x0)^2 > 0/(sin.x0)^2 by A2,REAL_1:73;
    then -(cos.x0/(sin.x0)^2) < -0 by XREAL_1:26;
    hence diff(cosec,x0) < 0 by A1,Th8;
  end;
  then rng(cosec|].0,PI/2.[) is open by Th8,FDIFF_2:41;
  hence cosec.:].0,PI/2.[ is open by RELAT_1:148;
end;

theorem
  arcsec1 is_continuous_on sec.:].0,PI/2.[ by Th121,FDIFF_1:33;

theorem
  arcsec2 is_continuous_on sec.:].PI/2,PI.[ by Th122,FDIFF_1:33;

theorem
  arccosec1 is_continuous_on cosec.:].-PI/2,0.[ by Th123,FDIFF_1:33;

theorem
  arccosec2 is_continuous_on cosec.:].0,PI/2.[ by Th124,FDIFF_1:33;