sincos10.miz



    begin

    reserve x,x0,r,r1,r2 for Real,

th for Real,

rr for set,

rseq for Real_Sequence;

    

     Lm1: [. 0 , ( PI / 2).[ c= ].( - ( PI / 2)), ( PI / 2).[

    proof

      

       A1: 0 in ].( - ( PI / 2)), ( PI / 2).[;

      

       A2: { 0 } c= ].( - ( PI / 2)), ( PI / 2).[ by A1, TARSKI:def 1;

       ]. 0 , ( PI / 2).[ c= ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 46;

      then ( ]. 0 , ( PI / 2).[ \/ { 0 }) c= ].( - ( PI / 2)), ( PI / 2).[ by A2, XBOOLE_1: 8;

      hence thesis by XXREAL_1: 131;

    end;

    theorem :: SINCOS10:1

    

     Th1: [. 0 , ( PI / 2).[ c= ( dom sec )

    proof

      ( [. 0 , ( PI / 2).[ /\ ( cos " { 0 })) = {}

      proof

        assume ( [. 0 , ( PI / 2).[ /\ ( cos " { 0 })) <> {} ;

        then

        consider rr be object such that

         A1: rr in ( [. 0 , ( PI / 2).[ /\ ( cos " { 0 })) by XBOOLE_0:def 1;

        rr in ( cos " { 0 }) by A1, XBOOLE_0:def 4;

        then

         A2: ( cos . rr) in { 0 } by FUNCT_1:def 7;

        rr in [. 0 , ( PI / 2).[ by A1, XBOOLE_0:def 4;

        then ( cos . rr) <> 0 by Lm1, COMPTRIG: 11;

        hence contradiction by A2, TARSKI:def 1;

      end;

      then ( [. 0 , ( PI / 2).[ \ ( cos " { 0 })) c= (( dom cos ) \ ( cos " { 0 })) & [. 0 , ( PI / 2).[ misses ( cos " { 0 }) by SIN_COS: 24, XBOOLE_0:def 7, XBOOLE_1: 33;

      then [. 0 , ( PI / 2).[ c= (( dom cos ) \ ( cos " { 0 })) by XBOOLE_1: 83;

      hence thesis by RFUNCT_1:def 2;

    end;

    

     Lm2: ].( PI / 2), PI .] c= ].( PI / 2), ((3 / 2) * PI ).[

    proof

      

       A1: ( PI / 2) < ( PI / 1) by XREAL_1: 76;

      

       A2: PI < ((3 / 2) * PI ) by XREAL_1: 155;

      then

       A3: PI in ].( PI / 2), ((3 / 2) * PI ).[ by A1;

      

       A4: { PI } c= ].( PI / 2), ((3 / 2) * PI ).[ by A3, TARSKI:def 1;

       ].( PI / 2), PI .[ c= ].( PI / 2), ((3 / 2) * PI ).[ by A2, XXREAL_1: 46;

      then ( ].( PI / 2), PI .[ \/ { PI }) c= ].( PI / 2), ((3 / 2) * PI ).[ by A4, XBOOLE_1: 8;

      hence thesis by A1, XXREAL_1: 132;

    end;

    theorem :: SINCOS10:2

    

     Th2: ].( PI / 2), PI .] c= ( dom sec )

    proof

      ( ].( PI / 2), PI .] /\ ( cos " { 0 })) = {}

      proof

        assume ( ].( PI / 2), PI .] /\ ( cos " { 0 })) <> {} ;

        then

        consider rr be object such that

         A1: rr in ( ].( PI / 2), PI .] /\ ( cos " { 0 })) by XBOOLE_0:def 1;

        rr in ( cos " { 0 }) by A1, XBOOLE_0:def 4;

        then

         A2: ( cos . rr) in { 0 } by FUNCT_1:def 7;

        rr in ].( PI / 2), PI .] by A1, XBOOLE_0:def 4;

        then ( cos . rr) <> 0 by Lm2, COMPTRIG: 13;

        hence contradiction by A2, TARSKI:def 1;

      end;

      then ( ].( PI / 2), PI .] \ ( cos " { 0 })) c= (( dom cos ) \ ( cos " { 0 })) & ].( PI / 2), PI .] misses ( cos " { 0 }) by SIN_COS: 24, XBOOLE_0:def 7, XBOOLE_1: 33;

      then ].( PI / 2), PI .] c= (( dom cos ) \ ( cos " { 0 })) by XBOOLE_1: 83;

      hence thesis by RFUNCT_1:def 2;

    end;

    

     Lm3: [.( - ( PI / 2)), 0 .[ c= ].( - PI ), 0 .[

    proof

      ( PI / 2) < ( PI / 1) by XREAL_1: 76;

      then

       A1: ( - PI ) < ( - ( PI / 2)) by XREAL_1: 24;

      then

       A2: ( - ( PI / 2)) in ].( - PI ), 0 .[;

      

       A3: {( - ( PI / 2))} c= ].( - PI ), 0 .[ by A2, TARSKI:def 1;

       ].( - ( PI / 2)), 0 .[ c= ].( - PI ), 0 .[ by A1, XXREAL_1: 46;

      then ( ].( - ( PI / 2)), 0 .[ \/ {( - ( PI / 2))}) c= ].( - PI ), 0 .[ by A3, XBOOLE_1: 8;

      hence thesis by XXREAL_1: 131;

    end;

    theorem :: SINCOS10:3

    

     Th3: [.( - ( PI / 2)), 0 .[ c= ( dom cosec )

    proof

      ( [.( - ( PI / 2)), 0 .[ /\ ( sin " { 0 })) = {}

      proof

        assume ( [.( - ( PI / 2)), 0 .[ /\ ( sin " { 0 })) <> {} ;

        then

        consider rr be object such that

         A1: rr in ( [.( - ( PI / 2)), 0 .[ /\ ( sin " { 0 })) by XBOOLE_0:def 1;

        

         A2: rr in ( sin " { 0 }) by A1, XBOOLE_0:def 4;

        

         A3: rr in [.( - ( PI / 2)), 0 .[ by A1, XBOOLE_0:def 4;

        reconsider rr as Real by A1;

        rr < 0 by A3, Lm3, XXREAL_1: 4;

        then

         A4: (rr + (2 * PI )) < ( 0 + (2 * PI )) by XREAL_1: 8;

        ( - PI ) < rr by A3, Lm3, XXREAL_1: 4;

        then (( - PI ) + (2 * PI )) < (rr + (2 * PI )) by XREAL_1: 8;

        then (rr + (2 * PI )) in ]. PI , (2 * PI ).[ by A4;

        then ( sin . (rr + (2 * PI ))) < 0 by COMPTRIG: 9;

        then

         A5: ( sin . rr) <> 0 by SIN_COS: 78;

        ( sin . rr) in { 0 } by A2, FUNCT_1:def 7;

        hence contradiction by A5, TARSKI:def 1;

      end;

      then ( [.( - ( PI / 2)), 0 .[ \ ( sin " { 0 })) c= (( dom sin ) \ ( sin " { 0 })) & [.( - ( PI / 2)), 0 .[ misses ( sin " { 0 }) by SIN_COS: 24, XBOOLE_0:def 7, XBOOLE_1: 33;

      then [.( - ( PI / 2)), 0 .[ c= (( dom sin ) \ ( sin " { 0 })) by XBOOLE_1: 83;

      hence thesis by RFUNCT_1:def 2;

    end;

    

     Lm4: ]. 0 , ( PI / 2).] c= ]. 0 , PI .[

    proof

      

       A1: ( PI / 2) < ( PI / 1) by XREAL_1: 76;

      then

       A2: ( PI / 2) in ]. 0 , PI .[;

      

       A3: {( PI / 2)} c= ]. 0 , PI .[ by A2, TARSKI:def 1;

       ]. 0 , ( PI / 2).[ c= ]. 0 , PI .[ by A1, XXREAL_1: 46;

      then ( ]. 0 , ( PI / 2).[ \/ {( PI / 2)}) c= ]. 0 , PI .[ by A3, XBOOLE_1: 8;

      hence thesis by XXREAL_1: 132;

    end;

    theorem :: SINCOS10:4

    

     Th4: ]. 0 , ( PI / 2).] c= ( dom cosec )

    proof

      ( ]. 0 , ( PI / 2).] /\ ( sin " { 0 })) = {}

      proof

        assume ( ]. 0 , ( PI / 2).] /\ ( sin " { 0 })) <> {} ;

        then

        consider rr be object such that

         A1: rr in ( ]. 0 , ( PI / 2).] /\ ( sin " { 0 })) by XBOOLE_0:def 1;

        rr in ( sin " { 0 }) by A1, XBOOLE_0:def 4;

        then

         A2: ( sin . rr) in { 0 } by FUNCT_1:def 7;

        rr in ]. 0 , ( PI / 2).] by A1, XBOOLE_0:def 4;

        then ( sin . rr) <> 0 by Lm4, COMPTRIG: 7;

        hence contradiction by A2, TARSKI:def 1;

      end;

      then ( ]. 0 , ( PI / 2).] \ ( sin " { 0 })) c= (( dom sin ) \ ( sin " { 0 })) & ]. 0 , ( PI / 2).] misses ( sin " { 0 }) by SIN_COS: 24, XBOOLE_0:def 7, XBOOLE_1: 33;

      then ]. 0 , ( PI / 2).] c= (( dom sin ) \ ( sin " { 0 })) by XBOOLE_1: 83;

      hence thesis by RFUNCT_1:def 2;

    end;

    theorem :: SINCOS10:5

    

     Th5: sec is_differentiable_on ]. 0 , ( PI / 2).[ & for x st x in ]. 0 , ( PI / 2).[ holds ( diff ( sec ,x)) = (( sin . x) / (( cos . x) ^2 ))

    proof

      set Z = ]. 0 , ( PI / 2).[;

       [. 0 , ( PI / 2).[ = (Z \/ { 0 }) by XXREAL_1: 131;

      then Z c= [. 0 , ( PI / 2).[ by XBOOLE_1: 7;

      then

       A1: Z c= ( dom sec ) by Th1;

      then

       A2: sec is_differentiable_on Z by FDIFF_9: 4;

      for x st x in Z holds ( diff ( sec ,x)) = (( sin . x) / (( cos . x) ^2 ))

      proof

        let x;

        assume

         A3: x in Z;

        

        then ( diff ( sec ,x)) = (( sec `| Z) . x) by A2, FDIFF_1:def 7

        .= (( sin . x) / (( cos . x) ^2 )) by A1, A3, FDIFF_9: 4;

        hence thesis;

      end;

      hence thesis by A1, FDIFF_9: 4;

    end;

    theorem :: SINCOS10:6

    

     Th6: sec is_differentiable_on ].( PI / 2), PI .[ & for x st x in ].( PI / 2), PI .[ holds ( diff ( sec ,x)) = (( sin . x) / (( cos . x) ^2 ))

    proof

      set Z = ].( PI / 2), PI .[;

      ( PI / 2) < ( PI / 1) by XREAL_1: 76;

      then ].( PI / 2), PI .] = (Z \/ { PI }) by XXREAL_1: 132;

      then Z c= ].( PI / 2), PI .] by XBOOLE_1: 7;

      then

       A1: Z c= ( dom sec ) by Th2;

      then

       A2: sec is_differentiable_on Z by FDIFF_9: 4;

      for x st x in Z holds ( diff ( sec ,x)) = (( sin . x) / (( cos . x) ^2 ))

      proof

        let x;

        assume

         A3: x in Z;

        

        then ( diff ( sec ,x)) = (( sec `| Z) . x) by A2, FDIFF_1:def 7

        .= (( sin . x) / (( cos . x) ^2 )) by A1, A3, FDIFF_9: 4;

        hence thesis;

      end;

      hence thesis by A1, FDIFF_9: 4;

    end;

    theorem :: SINCOS10:7

    

     Th7: cosec is_differentiable_on ].( - ( PI / 2)), 0 .[ & for x st x in ].( - ( PI / 2)), 0 .[ holds ( diff ( cosec ,x)) = ( - (( cos . x) / (( sin . x) ^2 )))

    proof

      set Z = ].( - ( PI / 2)), 0 .[;

       [.( - ( PI / 2)), 0 .[ = (Z \/ {( - ( PI / 2))}) by XXREAL_1: 131;

      then Z c= [.( - ( PI / 2)), 0 .[ by XBOOLE_1: 7;

      then

       A1: Z c= ( dom cosec ) by Th3;

      then

       A2: cosec is_differentiable_on Z by FDIFF_9: 5;

      for x st x in Z holds ( diff ( cosec ,x)) = ( - (( cos . x) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A3: x in Z;

        

        then ( diff ( cosec ,x)) = (( cosec `| Z) . x) by A2, FDIFF_1:def 7

        .= ( - (( cos . x) / (( sin . x) ^2 ))) by A1, A3, FDIFF_9: 5;

        hence thesis;

      end;

      hence thesis by A1, FDIFF_9: 5;

    end;

    theorem :: SINCOS10:8

    

     Th8: cosec is_differentiable_on ]. 0 , ( PI / 2).[ & for x st x in ]. 0 , ( PI / 2).[ holds ( diff ( cosec ,x)) = ( - (( cos . x) / (( sin . x) ^2 )))

    proof

      set Z = ]. 0 , ( PI / 2).[;

       ]. 0 , ( PI / 2).] = (Z \/ {( PI / 2)}) by XXREAL_1: 132;

      then Z c= ]. 0 , ( PI / 2).] by XBOOLE_1: 7;

      then

       A1: Z c= ( dom cosec ) by Th4;

      then

       A2: cosec is_differentiable_on Z by FDIFF_9: 5;

      for x st x in Z holds ( diff ( cosec ,x)) = ( - (( cos . x) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A3: x in Z;

        

        then ( diff ( cosec ,x)) = (( cosec `| Z) . x) by A2, FDIFF_1:def 7

        .= ( - (( cos . x) / (( sin . x) ^2 ))) by A1, A3, FDIFF_9: 5;

        hence thesis;

      end;

      hence thesis by A1, FDIFF_9: 5;

    end;

    theorem :: SINCOS10:9

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

    theorem :: SINCOS10:10

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

    theorem :: SINCOS10:11

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

    theorem :: SINCOS10:12

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

    

     Lm5: 0 in [. 0 , ( PI / 2).[ & ( PI / 4) in [. 0 , ( PI / 2).[

    proof

      ( PI / 4) < ( PI / 2) by XREAL_1: 76;

      hence thesis;

    end;

    

     Lm6: ((3 / 4) * PI ) in ].( PI / 2), PI .] & PI in ].( PI / 2), PI .]

    proof

      ( PI / 4) < ( PI / 2) by XREAL_1: 76;

      then (( PI / 4) + ( PI / 2)) > ( 0 + ( PI / 2)) & (( PI / 4) + ( PI / 2)) < (( PI / 2) + ( PI / 2)) by XREAL_1: 8;

      hence thesis by COMPTRIG: 5;

    end;

    

     Lm7: ( - ( PI / 2)) in [.( - ( PI / 2)), 0 .[ & ( - ( PI / 4)) in [.( - ( PI / 2)), 0 .[

    proof

      ( PI / 4) < ( PI / 2) by XREAL_1: 76;

      then ( - ( PI / 4)) > ( - ( PI / 2)) by XREAL_1: 24;

      hence thesis;

    end;

    

     Lm8: ( PI / 4) in ]. 0 , ( PI / 2).] & ( PI / 2) in ]. 0 , ( PI / 2).]

    proof

      ( PI / 4) < ( PI / 2) by XREAL_1: 76;

      hence thesis;

    end;

    

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

    then

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

    

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

    then

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

    

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

    

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

    

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

    then

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

    

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

    then

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

    

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

    

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

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

    then

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

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

    then

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

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

    then

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

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

    then

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

    theorem :: SINCOS10:13

    

     Th13: ( sec | ]. 0 , ( PI / 2).[) is increasing

    proof

      for x st x in ]. 0 , ( PI / 2).[ holds ( diff ( sec ,x)) > 0

      proof

        let x;

        assume

         A1: x in ]. 0 , ( PI / 2).[;

         ]. 0 , ( PI / 2).[ c= ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 46;

        then

         A2: ( cos . x) > 0 by A1, COMPTRIG: 11;

        ( PI / 2) < ( PI / 1) by XREAL_1: 76;

        then ]. 0 , ( PI / 2).[ c= ]. 0 , PI .[ by XXREAL_1: 46;

        then ( sin . x) > 0 by A1, COMPTRIG: 7;

        then (( sin . x) / (( cos . x) ^2 )) > ( 0 / (( cos . x) ^2 )) by A2;

        hence thesis by A1, Th5;

      end;

      hence thesis by Lm9, Th1, Th5, ROLLE: 9, XBOOLE_1: 1;

    end;

    theorem :: SINCOS10:14

    

     Th14: ( sec | ].( PI / 2), PI .[) is increasing

    proof

      for x st x in ].( PI / 2), PI .[ holds ( diff ( sec ,x)) > 0

      proof

        let x;

        assume

         A1: x in ].( PI / 2), PI .[;

         PI <= ((3 / 2) * PI ) by XREAL_1: 151;

        then ].( PI / 2), PI .[ c= ].( PI / 2), ((3 / 2) * PI ).[ by XXREAL_1: 46;

        then

         A2: ( cos . x) < 0 by A1, COMPTRIG: 13;

         ].( PI / 2), PI .[ c= ]. 0 , PI .[ by XXREAL_1: 46;

        then ( sin . x) > 0 by A1, COMPTRIG: 7;

        then (( sin . x) / (( cos . x) ^2 )) > ( 0 / (( cos . x) ^2 )) by A2;

        hence thesis by A1, Th6;

      end;

      hence thesis by Lm11, Th2, Th6, ROLLE: 9, XBOOLE_1: 1;

    end;

    theorem :: SINCOS10:15

    

     Th15: ( cosec | ].( - ( PI / 2)), 0 .[) is decreasing

    proof

      for x st x in ].( - ( PI / 2)), 0 .[ holds ( diff ( cosec ,x)) < 0

      proof

        let x;

        assume

         A1: x in ].( - ( PI / 2)), 0 .[;

        then x < 0 by XXREAL_1: 4;

        then

         A2: (x + (2 * PI )) < ( 0 + (2 * PI )) by XREAL_1: 8;

        ( ].( - ( PI / 2)), 0 .[ \/ {( - ( PI / 2))}) = [.( - ( PI / 2)), 0 .[ by XXREAL_1: 131;

        then ].( - ( PI / 2)), 0 .[ c= [.( - ( PI / 2)), 0 .[ by XBOOLE_1: 7;

        then ].( - ( PI / 2)), 0 .[ c= ].( - PI ), 0 .[ by Lm3;

        then ( - PI ) < x by A1, XXREAL_1: 4;

        then (( - PI ) + (2 * PI )) < (x + (2 * PI )) by XREAL_1: 8;

        then (x + (2 * PI )) in ]. PI , (2 * PI ).[ by A2;

        then ( sin . (x + (2 * PI ))) < 0 by COMPTRIG: 9;

        then

         A3: ( sin . x) < 0 by SIN_COS: 78;

         ].( - ( PI / 2)), 0 .[ c= ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 46;

        then ( cos . x) > 0 by A1, COMPTRIG: 11;

        then ( - (( cos . x) / (( sin . x) ^2 ))) < ( - 0 ) by A3;

        hence thesis by A1, Th7;

      end;

      hence thesis by Lm15, Th3, Th7, ROLLE: 10, XBOOLE_1: 1;

    end;

    theorem :: SINCOS10:16

    

     Th16: ( cosec | ]. 0 , ( PI / 2).[) is decreasing

    proof

      for x st x in ]. 0 , ( PI / 2).[ holds ( diff ( cosec ,x)) < 0

      proof

        let x;

        assume

         A1: x in ]. 0 , ( PI / 2).[;

         ]. 0 , ( PI / 2).[ c= ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 46;

        then

         A2: ( cos . x) > 0 by A1, COMPTRIG: 11;

         ]. 0 , ( PI / 2).[ c= ]. 0 , PI .[ by COMPTRIG: 5, XXREAL_1: 46;

        then ( sin . x) > 0 by A1, COMPTRIG: 7;

        then ( - (( cos . x) / (( sin . x) ^2 ))) < ( - 0 ) by A2;

        hence thesis by A1, Th8;

      end;

      hence thesis by Lm17, Th4, Th8, ROLLE: 10, XBOOLE_1: 1;

    end;

    theorem :: SINCOS10:17

    

     Th17: ( sec | [. 0 , ( PI / 2).[) is increasing

    proof

      now

        let r1, r2;

        assume that

         A1: r1 in ( [. 0 , ( PI / 2).[ /\ ( dom sec )) and

         A2: r2 in ( [. 0 , ( PI / 2).[ /\ ( dom sec )) and

         A3: r1 < r2;

        

         A4: r1 in ( dom sec ) by A1, XBOOLE_0:def 4;

        

         A5: r1 in [. 0 , ( PI / 2).[ by A1, XBOOLE_0:def 4;

        then

         A6: r1 < ( PI / 2) by XXREAL_1: 3;

        

         A7: r2 in ( dom sec ) by A2, XBOOLE_0:def 4;

        

         A8: r2 in [. 0 , ( PI / 2).[ by A2, XBOOLE_0:def 4;

        then

         A9: r2 < ( PI / 2) by XXREAL_1: 3;

        now

          per cases by A5, XXREAL_1: 3;

            suppose

             A10: 0 = r1;

            r2 < ( PI / 2) & ( PI / 2) < (2 * PI ) by A8, Lm1, XREAL_1: 68, XXREAL_1: 4;

            then r2 < (2 * PI ) by XXREAL_0: 2;

            then ( cos r2) < 1 by A3, A10, SIN_COS6: 34;

            then

             A11: ( cos . r2) < 1 by SIN_COS:def 19;

            (( - ( PI / 2)) + ((2 * PI ) * 0 )) < r2 & r2 < (( PI / 2) + ((2 * PI ) * 0 )) by A8, Lm1, XXREAL_1: 4;

            then ( cos r2) > 0 by SIN_COS6: 13;

            then ( cos . r2) > 0 by SIN_COS:def 19;

            then

             A12: (1 / 1) < (1 / ( cos . r2)) by A11, XREAL_1: 76;

            ( sec . r1) = (1 / 1) by A4, A10, RFUNCT_1:def 2, SIN_COS: 30

            .= 1;

            hence ( sec . r2) > ( sec . r1) by A7, A12, RFUNCT_1:def 2;

          end;

            suppose

             A13: 0 < r1;

            then r1 in ]. 0 , ( PI / 2).[ by A6;

            then

             A14: r1 in ( ]. 0 , ( PI / 2).[ /\ ( dom sec )) by A4, XBOOLE_0:def 4;

            r2 in ]. 0 , ( PI / 2).[ by A3, A9, A13;

            then r2 in ( ]. 0 , ( PI / 2).[ /\ ( dom sec )) by A7, XBOOLE_0:def 4;

            hence ( sec . r2) > ( sec . r1) by A3, A14, Th13, RFUNCT_2: 20;

          end;

        end;

        hence ( sec . r2) > ( sec . r1);

      end;

      hence thesis by RFUNCT_2: 20;

    end;

    theorem :: SINCOS10:18

    

     Th18: ( sec | ].( PI / 2), PI .]) is increasing

    proof

      now

        let r1, r2;

        assume that

         A1: r1 in ( ].( PI / 2), PI .] /\ ( dom sec )) and

         A2: r2 in ( ].( PI / 2), PI .] /\ ( dom sec )) and

         A3: r1 < r2;

        

         A4: r1 in ( dom sec ) by A1, XBOOLE_0:def 4;

        

         A5: r2 in ( dom sec ) by A2, XBOOLE_0:def 4;

        

         A6: r1 in ].( PI / 2), PI .] by A1, XBOOLE_0:def 4;

        then

         A7: ( PI / 2) < r1 by XXREAL_1: 2;

        

         A8: r2 in ].( PI / 2), PI .] by A2, XBOOLE_0:def 4;

        then

         A9: r2 <= PI by XXREAL_1: 2;

        

         A10: ( PI / 2) < r2 by A8, XXREAL_1: 2;

        now

          per cases by A9, XXREAL_0: 1;

            suppose

             A11: r2 < PI ;

            then r1 < PI by A3, XXREAL_0: 2;

            then r1 in ].( PI / 2), PI .[ by A7;

            then

             A12: r1 in ( ].( PI / 2), PI .[ /\ ( dom sec )) by A4, XBOOLE_0:def 4;

            r2 in ].( PI / 2), PI .[ by A10, A11;

            then r2 in ( ].( PI / 2), PI .[ /\ ( dom sec )) by A5, XBOOLE_0:def 4;

            hence ( sec . r2) > ( sec . r1) by A3, A12, Th14, RFUNCT_2: 20;

          end;

            suppose

             A13: r2 = PI ;

            ( PI * 1) < ( PI * (3 / 2)) by XREAL_1: 68;

            then

             A14: r1 < (((3 / 2) * PI ) + ((2 * PI ) * 0 )) by A3, A13, XXREAL_0: 2;

            (( PI / 2) + ((2 * PI ) * 0 )) < r1 by A6, XXREAL_1: 2;

            then ( cos r1) < 0 by A14, SIN_COS6: 14;

            then

             A15: ( cos . r1) < 0 by SIN_COS:def 19;

            r1 < PI by A3, A9, XXREAL_0: 2;

            then ( cos r1) > ( - 1) by A7, SIN_COS6: 35;

            then ( cos . r1) > ( - 1) by SIN_COS:def 19;

            then

             A16: (( cos . r1) " ) < (( - 1) " ) by A15, XREAL_1: 87;

            ( sec . r2) = (1 / ( - 1)) by A5, A13, RFUNCT_1:def 2, SIN_COS: 76

            .= ( - 1);

            hence ( sec . r1) < ( sec . r2) by A4, A16, RFUNCT_1:def 2;

          end;

        end;

        hence ( sec . r2) > ( sec . r1);

      end;

      hence thesis by RFUNCT_2: 20;

    end;

    theorem :: SINCOS10:19

    

     Th19: ( cosec | [.( - ( PI / 2)), 0 .[) is decreasing

    proof

      now

        let r1, r2;

        assume that

         A1: r1 in ( [.( - ( PI / 2)), 0 .[ /\ ( dom cosec )) and

         A2: r2 in ( [.( - ( PI / 2)), 0 .[ /\ ( dom cosec )) and

         A3: r1 < r2;

        

         A4: r1 in ( dom cosec ) by A1, XBOOLE_0:def 4;

        

         A5: r1 in [.( - ( PI / 2)), 0 .[ by A1, XBOOLE_0:def 4;

        then

         A6: r1 < 0 by XXREAL_1: 3;

        

         A7: r2 in ( dom cosec ) by A2, XBOOLE_0:def 4;

        

         A8: r2 in [.( - ( PI / 2)), 0 .[ by A2, XBOOLE_0:def 4;

        then

         A9: r2 < 0 by XXREAL_1: 3;

        

         A10: ( - ( PI / 2)) <= r1 by A5, XXREAL_1: 3;

        now

          per cases by A10, XXREAL_0: 1;

            suppose

             A11: ( - ( PI / 2)) = r1;

            ( - ( PI / 2)) > ( - PI ) by COMPTRIG: 5, XREAL_1: 24;

            then

             A12: ].( - ( PI / 2)), 0 .[ c= ].( - PI ), 0 .[ by XXREAL_1: 46;

            r2 in ].( - ( PI / 2)), 0 .[ by A3, A9, A11;

            then ( - PI ) < r2 by A12, XXREAL_1: 4;

            then

             A13: (( - PI ) + (2 * PI )) < (r2 + (2 * PI )) by XREAL_1: 8;

            (r2 + (2 * PI )) < ( 0 + (2 * PI )) by A9, XREAL_1: 8;

            then (r2 + (2 * PI )) in ]. PI , (2 * PI ).[ by A13;

            then ( sin . (r2 + (2 * PI ))) < 0 by COMPTRIG: 9;

            then

             A14: ( sin . r2) < 0 by SIN_COS: 78;

            

             A15: r2 < ((2 * PI ) + ((2 * PI ) * ( - 1))) by A8, XXREAL_1: 3;

            (((3 / 2) * PI ) + ((2 * PI ) * ( - 1))) < r2 by A3, A11;

            then ( sin r2) > ( - 1) by A15, SIN_COS6: 39;

            then ( sin . r2) > ( - 1) by SIN_COS:def 17;

            then

             A16: (( sin . r2) " ) < (( - 1) " ) by A14, XREAL_1: 87;

            ( cosec . r1) = (1 / ( sin . ( - ( PI / 2)))) by A4, A11, RFUNCT_1:def 2

            .= (1 / ( - 1)) by SIN_COS: 30, SIN_COS: 76

            .= ( - 1);

            hence ( cosec . r2) < ( cosec . r1) by A7, A16, RFUNCT_1:def 2;

          end;

            suppose

             A17: ( - ( PI / 2)) < r1;

            then ( - ( PI / 2)) < r2 by A3, XXREAL_0: 2;

            then r2 in ].( - ( PI / 2)), 0 .[ by A9;

            then

             A18: r2 in ( ].( - ( PI / 2)), 0 .[ /\ ( dom cosec )) by A7, XBOOLE_0:def 4;

            r1 in ].( - ( PI / 2)), 0 .[ by A6, A17;

            then r1 in ( ].( - ( PI / 2)), 0 .[ /\ ( dom cosec )) by A4, XBOOLE_0:def 4;

            hence ( cosec . r2) < ( cosec . r1) by A3, A18, Th15, RFUNCT_2: 21;

          end;

        end;

        hence ( cosec . r2) < ( cosec . r1);

      end;

      hence thesis by RFUNCT_2: 21;

    end;

    theorem :: SINCOS10:20

    

     Th20: ( cosec | ]. 0 , ( PI / 2).]) is decreasing

    proof

      now

        let r1, r2;

        assume that

         A1: r1 in ( ]. 0 , ( PI / 2).] /\ ( dom cosec )) and

         A2: r2 in ( ]. 0 , ( PI / 2).] /\ ( dom cosec )) and

         A3: r1 < r2;

        

         A4: r1 in ( dom cosec ) by A1, XBOOLE_0:def 4;

        

         A5: r2 in ]. 0 , ( PI / 2).] by A2, XBOOLE_0:def 4;

        then

         A6: r2 <= ( PI / 2) by XXREAL_1: 2;

        

         A7: r2 in ( dom cosec ) by A2, XBOOLE_0:def 4;

        

         A8: r1 in ]. 0 , ( PI / 2).] by A1, XBOOLE_0:def 4;

        then

         A9: 0 < r1 by XXREAL_1: 2;

        

         A10: 0 < r2 by A5, XXREAL_1: 2;

        now

          per cases by A6, XXREAL_0: 1;

            suppose

             A11: r2 < ( PI / 2);

            then r1 < ( PI / 2) by A3, XXREAL_0: 2;

            then r1 in ]. 0 , ( PI / 2).[ by A9;

            then

             A12: r1 in ( ]. 0 , ( PI / 2).[ /\ ( dom cosec )) by A4, XBOOLE_0:def 4;

            r2 in ]. 0 , ( PI / 2).[ by A10, A11;

            then r2 in ( ]. 0 , ( PI / 2).[ /\ ( dom cosec )) by A7, XBOOLE_0:def 4;

            hence ( cosec . r2) < ( cosec . r1) by A3, A12, Th16, RFUNCT_2: 21;

          end;

            suppose

             A13: r2 = ( PI / 2);

            then ( sin r1) < 1 by A3, A9, SIN_COS6: 30;

            then

             A14: ( sin . r1) < 1 by SIN_COS:def 17;

            ( sin . r1) > 0 by A8, Lm4, COMPTRIG: 7;

            then

             A15: (1 / 1) < (1 / ( sin . r1)) by A14, XREAL_1: 76;

            ( cosec . r2) = (1 / 1) by A7, A13, RFUNCT_1:def 2, SIN_COS: 76

            .= 1;

            hence ( cosec . r2) < ( cosec . r1) by A4, A15, RFUNCT_1:def 2;

          end;

        end;

        hence ( cosec . r2) < ( cosec . r1);

      end;

      hence thesis by RFUNCT_2: 21;

    end;

    theorem :: SINCOS10:21

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

    theorem :: SINCOS10:22

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

    theorem :: SINCOS10:23

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

    theorem :: SINCOS10:24

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

    registration

      cluster ( sec | [. 0 , ( PI / 2).[) -> one-to-one;

      coherence by Th17, FCONT_3: 8;

      cluster ( sec | ].( PI / 2), PI .]) -> one-to-one;

      coherence by Th18, FCONT_3: 8;

      cluster ( cosec | [.( - ( PI / 2)), 0 .[) -> one-to-one;

      coherence by Th19, FCONT_3: 8;

      cluster ( cosec | ]. 0 , ( PI / 2).]) -> one-to-one;

      coherence by Th20, FCONT_3: 8;

    end

    definition

      :: SINCOS10:def1

      func arcsec1 -> PartFunc of REAL , REAL equals (( sec | [. 0 , ( PI / 2).[) " );

      coherence ;

      :: SINCOS10:def2

      func arcsec2 -> PartFunc of REAL , REAL equals (( sec | ].( PI / 2), PI .]) " );

      coherence ;

      :: SINCOS10:def3

      func arccosec1 -> PartFunc of REAL , REAL equals (( cosec | [.( - ( PI / 2)), 0 .[) " );

      coherence ;

      :: SINCOS10:def4

      func arccosec2 -> PartFunc of REAL , REAL equals (( cosec | ]. 0 , ( PI / 2).]) " );

      coherence ;

    end

    definition

      let r be Real;

      :: SINCOS10:def5

      func arcsec1 r -> number equals ( arcsec1 . r);

      coherence ;

      :: SINCOS10:def6

      func arcsec2 r -> number equals ( arcsec2 . r);

      coherence ;

      :: SINCOS10:def7

      func arccosec1 r -> number equals ( arccosec1 . r);

      coherence ;

      :: SINCOS10:def8

      func arccosec2 r -> number equals ( arccosec2 . r);

      coherence ;

    end

    registration

      let r be Real;

      cluster ( arcsec1 r) -> real;

      coherence ;

      cluster ( arcsec2 r) -> real;

      coherence ;

      cluster ( arccosec1 r) -> real;

      coherence ;

      cluster ( arccosec2 r) -> real;

      coherence ;

    end

    

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

    

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

    

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

    

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

    theorem :: SINCOS10:25

    

     Th25: ( rng arcsec1 ) = [. 0 , ( PI / 2).[

    proof

      ( dom ( sec | [. 0 , ( PI / 2).[)) = [. 0 , ( PI / 2).[ by Th1, RELAT_1: 62;

      hence thesis by FUNCT_1: 33;

    end;

    theorem :: SINCOS10:26

    

     Th26: ( rng arcsec2 ) = ].( PI / 2), PI .]

    proof

      ( dom ( sec | ].( PI / 2), PI .])) = ].( PI / 2), PI .] by Th2, RELAT_1: 62;

      hence thesis by FUNCT_1: 33;

    end;

    theorem :: SINCOS10:27

    

     Th27: ( rng arccosec1 ) = [.( - ( PI / 2)), 0 .[

    proof

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

      hence thesis by FUNCT_1: 33;

    end;

    theorem :: SINCOS10:28

    

     Th28: ( rng arccosec2 ) = ]. 0 , ( PI / 2).]

    proof

      ( dom ( cosec | ]. 0 , ( PI / 2).])) = ]. 0 , ( PI / 2).] by Th4, RELAT_1: 62;

      hence thesis by FUNCT_1: 33;

    end;

    registration

      cluster arcsec1 -> one-to-one;

      coherence ;

      cluster arcsec2 -> one-to-one;

      coherence ;

      cluster arccosec1 -> one-to-one;

      coherence ;

      cluster arccosec2 -> one-to-one;

      coherence ;

    end

    theorem :: SINCOS10:29

    

     Th29: ( sin . ( PI / 4)) = (1 / ( sqrt 2)) & ( cos . ( PI / 4)) = (1 / ( sqrt 2))

    proof

      

       A1: (( sqrt (1 / 2)) ^2 ) = (1 / 2) by SQUARE_1:def 2;

      1 = ((( sin . ( PI / 4)) ^2 ) + (( sin . ( PI / 4)) ^2 )) by SIN_COS: 28, SIN_COS: 73

      .= (2 * (( sin . ( PI / 4)) ^2 ));

      then

       A2: ( sin . ( PI / 4)) = ( sqrt (1 / 2)) or ( sin . ( PI / 4)) = ( - ( sqrt (1 / 2))) by A1, SQUARE_1: 40;

      ( PI / 4) < ( PI / 1) by XREAL_1: 76;

      then

       A3: ( PI / 4) in ]. 0 , PI .[;

      ( sqrt (1 / 2)) > 0 by SQUARE_1: 25;

      hence thesis by A2, A3, COMPTRIG: 7, SIN_COS: 73, SQUARE_1: 32;

    end;

    theorem :: SINCOS10:30

    

     Th30: ( sin . ( - ( PI / 4))) = ( - (1 / ( sqrt 2))) & ( cos . ( - ( PI / 4))) = (1 / ( sqrt 2)) & ( sin . ((3 / 4) * PI )) = (1 / ( sqrt 2)) & ( cos . ((3 / 4) * PI )) = ( - (1 / ( sqrt 2)))

    proof

      

       A1: ( cos . ( - ( PI / 4))) = (1 / ( sqrt 2)) by Th29, SIN_COS: 30;

      

       A2: ( cos . ((3 / 4) * PI )) = ( cos . ( PI + ( - ( PI / 4))))

      .= ( - (1 / ( sqrt 2))) by A1, SIN_COS: 78;

      

       A3: ( sin . ( - ( PI / 4))) = ( - (1 / ( sqrt 2))) by Th29, SIN_COS: 30;

      ( sin . ((3 / 4) * PI )) = ( sin . ( PI + ( - ( PI / 4))))

      .= ( - ( - (1 / ( sqrt 2)))) by A3, SIN_COS: 78

      .= (1 / ( sqrt 2));

      hence thesis by A2, Th29, SIN_COS: 30;

    end;

    theorem :: SINCOS10:31

    

     Th31: ( sec . 0 ) = 1 & ( sec . ( PI / 4)) = ( sqrt 2) & ( sec . ((3 / 4) * PI )) = ( - ( sqrt 2)) & ( sec . PI ) = ( - 1)

    proof

      

       A1: ( sec . PI ) = (1 / ( - 1)) by Lm6, Th2, RFUNCT_1:def 2, SIN_COS: 76

      .= ( - 1);

      

       A2: ( sec . ((3 / 4) * PI )) = (1 / ( - (1 / ( sqrt 2)))) by Lm6, Th2, Th30, RFUNCT_1:def 2

      .= ( - (1 / (1 / ( sqrt 2)))) by XCMPLX_1: 188

      .= ( - ( sqrt 2));

      

       A3: ( sec . 0 ) = (1 / 1) by Lm5, Th1, RFUNCT_1:def 2, SIN_COS: 30

      .= 1;

      ( sec . ( PI / 4)) = (1 / (1 / ( sqrt 2))) by Lm5, Th1, Th29, RFUNCT_1:def 2

      .= ( sqrt 2);

      hence thesis by A3, A2, A1;

    end;

    theorem :: SINCOS10:32

    

     Th32: ( cosec . ( - ( PI / 2))) = ( - 1) & ( cosec . ( - ( PI / 4))) = ( - ( sqrt 2)) & ( cosec . ( PI / 4)) = ( sqrt 2) & ( cosec . ( PI / 2)) = 1

    proof

      

       A1: ( cosec . ( PI / 2)) = (1 / 1) by Lm8, Th4, RFUNCT_1:def 2, SIN_COS: 76

      .= 1;

      

       A2: ( cosec . ( PI / 4)) = (1 / (1 / ( sqrt 2))) by Lm8, Th4, Th29, RFUNCT_1:def 2

      .= ( sqrt 2);

      

       A3: ( cosec . ( - ( PI / 2))) = (1 / ( sin . ( - ( PI / 2)))) by Lm7, Th3, RFUNCT_1:def 2

      .= (1 / ( - 1)) by SIN_COS: 30, SIN_COS: 76

      .= ( - 1);

      ( cosec . ( - ( PI / 4))) = (1 / ( - (1 / ( sqrt 2)))) by Lm7, Th3, Th30, RFUNCT_1:def 2

      .= ( - (1 / (1 / ( sqrt 2)))) by XCMPLX_1: 188

      .= ( - ( sqrt 2));

      hence thesis by A3, A2, A1;

    end;

    theorem :: SINCOS10:33

    

     Th33: for x be set st x in [. 0 , ( PI / 4).] holds ( sec . x) in [.1, ( sqrt 2).]

    proof

      let x be set;

      assume x in [. 0 , ( PI / 4).];

      then x in ( ]. 0 , ( PI / 4).[ \/ { 0 , ( PI / 4)}) by XXREAL_1: 128;

      then

       A1: x in ]. 0 , ( PI / 4).[ or x in { 0 , ( PI / 4)} by XBOOLE_0:def 3;

      per cases by A1, TARSKI:def 2;

        suppose

         A2: x in ]. 0 , ( PI / 4).[;

        ( PI / 4) < ( PI / 2) by XREAL_1: 76;

        then 0 in [. 0 , ( PI / 2).[ & ( PI / 4) in [. 0 , ( PI / 2).[;

        then

         A3: [. 0 , ( PI / 4).] c= [. 0 , ( PI / 2).[ by XXREAL_2:def 12;

        then

         A4: ( sec | [. 0 , ( PI / 4).]) is increasing by Th17, RFUNCT_2: 28;

        

         A5: ex s be Real st s = x & 0 < s & s < ( PI / 4) by A2;

        

         A6: ]. 0 , ( PI / 4).[ c= [. 0 , ( PI / 4).] by XXREAL_1: 25;

        

         A7: ( [. 0 , ( PI / 4).] /\ ( dom sec )) = [. 0 , ( PI / 4).] by A3, Th1, XBOOLE_1: 1, XBOOLE_1: 28;

         0 in [. 0 , ( PI / 4).] & ex s be Real st s = x & 0 < s & s < ( PI / 4) by A2;

        then

         A8: 1 < ( sec . x) by A2, A4, A7, A6, Th31, RFUNCT_2: 20;

        ( PI / 4) in ( [. 0 , ( PI / 4).] /\ ( dom sec )) by A7;

        then ( sec . x) < ( sqrt 2) by A2, A4, A7, A6, A5, Th31, RFUNCT_2: 20;

        hence thesis by A8;

      end;

        suppose x = 0 ;

        hence thesis by Th31, SQUARE_1: 19;

      end;

        suppose x = ( PI / 4);

        hence thesis by Th31, SQUARE_1: 19;

      end;

    end;

    theorem :: SINCOS10:34

    

     Th34: for x be set st x in [.((3 / 4) * PI ), PI .] holds ( sec . x) in [.( - ( sqrt 2)), ( - 1).]

    proof

      let x be set;

      

       A1: ( PI / 4) < ( PI / 2) by XREAL_1: 76;

      then

       A2: (( PI / 4) + ( PI / 2)) < (( PI / 2) + ( PI / 2)) by XREAL_1: 8;

      assume x in [.((3 / 4) * PI ), PI .];

      then x in ( ].((3 / 4) * PI ), PI .[ \/ {((3 / 4) * PI ), PI }) by A2, XXREAL_1: 128;

      then

       A3: x in ].((3 / 4) * PI ), PI .[ or x in {((3 / 4) * PI ), PI } by XBOOLE_0:def 3;

      per cases by A3, TARSKI:def 2;

        suppose

         A4: x in ].((3 / 4) * PI ), PI .[;

        (( PI / 4) + ( PI / 4)) < (( PI / 2) + ( PI / 4)) by A1, XREAL_1: 8;

        then

         A5: ((3 / 4) * PI ) in ].( PI / 2), PI .] by A2;

         PI in ].( PI / 2), PI .] by COMPTRIG: 5;

        then

         A6: [.((3 / 4) * PI ), PI .] c= ].( PI / 2), PI .] by A5, XXREAL_2:def 12;

        then

         A7: ( sec | [.((3 / 4) * PI ), PI .]) is increasing by Th18, RFUNCT_2: 28;

        

         A8: ex s be Real st s = x & ((3 / 4) * PI ) < s & s < PI by A4;

        

         A9: ex s be Real st s = x & ((3 / 4) * PI ) < s & s < PI by A4;

        

         A10: ].((3 / 4) * PI ), PI .[ c= [.((3 / 4) * PI ), PI .] by XXREAL_1: 25;

        

         A11: ( [.((3 / 4) * PI ), PI .] /\ ( dom sec )) = [.((3 / 4) * PI ), PI .] by A6, Th2, XBOOLE_1: 1, XBOOLE_1: 28;

        then PI in ( [.((3 / 4) * PI ), PI .] /\ ( dom sec )) by A2;

        then

         A12: ( sec . x) < ( - 1) by A4, A7, A11, A10, A9, Th31, RFUNCT_2: 20;

        ((3 / 4) * PI ) in [.((3 / 4) * PI ), PI .] by A2;

        then ( - ( sqrt 2)) < ( sec . x) by A4, A7, A11, A10, A8, Th31, RFUNCT_2: 20;

        hence thesis by A12;

      end;

        suppose

         A13: x = ((3 / 4) * PI );

        ( - ( sqrt 2)) < ( - 1) by SQUARE_1: 19, XREAL_1: 24;

        hence thesis by A13, Th31;

      end;

        suppose

         A14: x = PI ;

        ( - ( sqrt 2)) < ( - 1) by SQUARE_1: 19, XREAL_1: 24;

        hence thesis by A14, Th31;

      end;

    end;

    theorem :: SINCOS10:35

    

     Th35: for x be set st x in [.( - ( PI / 2)), ( - ( PI / 4)).] holds ( cosec . x) in [.( - ( sqrt 2)), ( - 1).]

    proof

      let x be set;

      ( PI / 4) < ( PI / 2) by XREAL_1: 76;

      then

       A1: ( - ( PI / 2)) < ( - ( PI / 4)) by XREAL_1: 24;

      assume x in [.( - ( PI / 2)), ( - ( PI / 4)).];

      then x in ( ].( - ( PI / 2)), ( - ( PI / 4)).[ \/ {( - ( PI / 2)), ( - ( PI / 4))}) by A1, XXREAL_1: 128;

      then

       A2: x in ].( - ( PI / 2)), ( - ( PI / 4)).[ or x in {( - ( PI / 2)), ( - ( PI / 4))} by XBOOLE_0:def 3;

      per cases by A2, TARSKI:def 2;

        suppose

         A3: x in ].( - ( PI / 2)), ( - ( PI / 4)).[;

        then

         A4: ex s be Real st s = x & ( - ( PI / 2)) < s & s < ( - ( PI / 4));

        

         A5: ex s be Real st s = x & ( - ( PI / 2)) < s & s < ( - ( PI / 4)) by A3;

        

         A6: ].( - ( PI / 2)), ( - ( PI / 4)).[ c= [.( - ( PI / 2)), ( - ( PI / 4)).] by XXREAL_1: 25;

        ( - ( PI / 2)) in [.( - ( PI / 2)), 0 .[ & ( - ( PI / 4)) in [.( - ( PI / 2)), 0 .[ by A1;

        then

         A7: [.( - ( PI / 2)), ( - ( PI / 4)).] c= [.( - ( PI / 2)), 0 .[ by XXREAL_2:def 12;

        then

         A8: ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) is decreasing by Th19, RFUNCT_2: 29;

        

         A9: ( [.( - ( PI / 2)), ( - ( PI / 4)).] /\ ( dom cosec )) = [.( - ( PI / 2)), ( - ( PI / 4)).] by A7, Th3, XBOOLE_1: 1, XBOOLE_1: 28;

        then ( - ( PI / 4)) in ( [.( - ( PI / 2)), ( - ( PI / 4)).] /\ ( dom cosec )) by A1;

        then

         A10: ( cosec . x) > ( - ( sqrt 2)) by A3, A8, A9, A6, A5, Th32, RFUNCT_2: 21;

        ( - ( PI / 2)) in [.( - ( PI / 2)), ( - ( PI / 4)).] by A1;

        then ( - 1) > ( cosec . x) by A3, A8, A9, A6, A4, Th32, RFUNCT_2: 21;

        hence thesis by A10;

      end;

        suppose

         A11: x = ( - ( PI / 2));

        ( - ( sqrt 2)) < ( - 1) by SQUARE_1: 19, XREAL_1: 24;

        hence thesis by A11, Th32;

      end;

        suppose

         A12: x = ( - ( PI / 4));

        ( - ( sqrt 2)) < ( - 1) by SQUARE_1: 19, XREAL_1: 24;

        hence thesis by A12, Th32;

      end;

    end;

    theorem :: SINCOS10:36

    

     Th36: for x be set st x in [.( PI / 4), ( PI / 2).] holds ( cosec . x) in [.1, ( sqrt 2).]

    proof

      let x be set;

      

       A1: ( PI / 4) < ( PI / 2) by XREAL_1: 76;

      assume x in [.( PI / 4), ( PI / 2).];

      then x in ( ].( PI / 4), ( PI / 2).[ \/ {( PI / 4), ( PI / 2)}) by A1, XXREAL_1: 128;

      then

       A2: x in ].( PI / 4), ( PI / 2).[ or x in {( PI / 4), ( PI / 2)} by XBOOLE_0:def 3;

      per cases by A2, TARSKI:def 2;

        suppose

         A3: x in ].( PI / 4), ( PI / 2).[;

        then

         A4: ex s be Real st s = x & ( PI / 4) < s & s < ( PI / 2);

        

         A5: ex s be Real st s = x & ( PI / 4) < s & s < ( PI / 2) by A3;

        

         A6: ].( PI / 4), ( PI / 2).[ c= [.( PI / 4), ( PI / 2).] by XXREAL_1: 25;

        ( PI / 4) in ]. 0 , ( PI / 2).] & ( PI / 2) in ]. 0 , ( PI / 2).] by A1;

        then

         A7: [.( PI / 4), ( PI / 2).] c= ]. 0 , ( PI / 2).] by XXREAL_2:def 12;

        then

         A8: ( cosec | [.( PI / 4), ( PI / 2).]) is decreasing by Th20, RFUNCT_2: 29;

        

         A9: ( [.( PI / 4), ( PI / 2).] /\ ( dom cosec )) = [.( PI / 4), ( PI / 2).] by A7, Th4, XBOOLE_1: 1, XBOOLE_1: 28;

        then ( PI / 2) in ( [.( PI / 4), ( PI / 2).] /\ ( dom cosec )) by A1;

        then

         A10: ( cosec . x) > 1 by A3, A8, A9, A6, A5, Th32, RFUNCT_2: 21;

        ( PI / 4) in [.( PI / 4), ( PI / 2).] by A1;

        then ( sqrt 2) > ( cosec . x) by A3, A8, A9, A6, A4, Th32, RFUNCT_2: 21;

        hence thesis by A10;

      end;

        suppose x = ( PI / 4);

        hence thesis by Th32, SQUARE_1: 19;

      end;

        suppose x = ( PI / 2);

        hence thesis by Th32, SQUARE_1: 19;

      end;

    end;

    

     Lm29: ( dom ( sec | [. 0 , ( PI / 4).])) = [. 0 , ( PI / 4).]

    proof

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

      hence thesis by Th1, RELAT_1: 62, XBOOLE_1: 1;

    end;

    

     Lm30: ( dom ( sec | [.((3 / 4) * PI ), PI .])) = [.((3 / 4) * PI ), PI .]

    proof

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

      hence thesis by Th2, RELAT_1: 62, XBOOLE_1: 1;

    end;

    

     Lm31: ( dom ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).])) = [.( - ( PI / 2)), ( - ( PI / 4)).]

    proof

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

      hence thesis by Th3, RELAT_1: 62, XBOOLE_1: 1;

    end;

    

     Lm32: ( dom ( cosec | [.( PI / 4), ( PI / 2).])) = [.( PI / 4), ( PI / 2).]

    proof

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

      hence thesis by Th4, RELAT_1: 62, XBOOLE_1: 1;

    end;

    

     Lm33: ( dom ( sec | [. 0 , ( PI / 2).[)) = [. 0 , ( PI / 2).[ & for th st th in [. 0 , ( PI / 2).[ holds (( sec | [. 0 , ( PI / 2).[) . th) = ( sec . th)

    proof

      ( dom ( sec | [. 0 , ( PI / 2).[)) = (( dom sec ) /\ [. 0 , ( PI / 2).[) by RELAT_1: 61;

      then ( dom ( sec | [. 0 , ( PI / 2).[)) = [. 0 , ( PI / 2).[ by Th1, XBOOLE_1: 28;

      hence thesis by FUNCT_1: 47;

    end;

    

     Lm34: ( dom ( sec | ].( PI / 2), PI .])) = ].( PI / 2), PI .] & for th st th in ].( PI / 2), PI .] holds (( sec | ].( PI / 2), PI .]) . th) = ( sec . th)

    proof

      ( dom ( sec | ].( PI / 2), PI .])) = (( dom sec ) /\ ].( PI / 2), PI .]) by RELAT_1: 61;

      then ( dom ( sec | ].( PI / 2), PI .])) = ].( PI / 2), PI .] by Th2, XBOOLE_1: 28;

      hence thesis by FUNCT_1: 47;

    end;

    

     Lm35: ( dom ( cosec | [.( - ( PI / 2)), 0 .[)) = [.( - ( PI / 2)), 0 .[ & for th st th in [.( - ( PI / 2)), 0 .[ holds (( cosec | [.( - ( PI / 2)), 0 .[) . th) = ( cosec . th)

    proof

      ( dom ( cosec | [.( - ( PI / 2)), 0 .[)) = (( dom cosec ) /\ [.( - ( PI / 2)), 0 .[) by RELAT_1: 61;

      then ( dom ( cosec | [.( - ( PI / 2)), 0 .[)) = [.( - ( PI / 2)), 0 .[ by Th3, XBOOLE_1: 28;

      hence thesis by FUNCT_1: 47;

    end;

    

     Lm36: ( dom ( cosec | ]. 0 , ( PI / 2).])) = ]. 0 , ( PI / 2).] & for th st th in ]. 0 , ( PI / 2).] holds (( cosec | ]. 0 , ( PI / 2).]) . th) = ( cosec . th)

    proof

      ( dom ( cosec | ]. 0 , ( PI / 2).])) = (( dom cosec ) /\ ]. 0 , ( PI / 2).]) by RELAT_1: 61;

      then ( dom ( cosec | ]. 0 , ( PI / 2).])) = ]. 0 , ( PI / 2).] by Th4, XBOOLE_1: 28;

      hence thesis by FUNCT_1: 47;

    end;

    theorem :: SINCOS10:37

    

     Th37: ( sec | [. 0 , ( PI / 2).[) is continuous

    proof

      for th be Real st th in ( dom ( sec | [. 0 , ( PI / 2).[)) holds ( sec | [. 0 , ( PI / 2).[) is_continuous_in th

      proof

        let th be Real;

        

         A1: cos is_differentiable_in th by SIN_COS: 63;

        assume

         A2: th in ( dom ( sec | [. 0 , ( PI / 2).[));

        then th in [. 0 , ( PI / 2).[ by RELAT_1: 57;

        then ( cos . th) <> 0 by Lm1, COMPTRIG: 11;

        then

         A3: sec is_continuous_in th by A1, FCONT_1: 10, FDIFF_1: 24;

        now

          let rseq;

          assume that

           A4: ( rng rseq) c= ( dom ( sec | [. 0 , ( PI / 2).[)) and

           A5: rseq is convergent & ( lim rseq) = th;

          

           A6: ( dom ( sec | [. 0 , ( PI / 2).[)) = [. 0 , ( PI / 2).[ by Th1, RELAT_1: 62;

          now

            let n be Element of NAT ;

            ( dom rseq) = NAT by SEQ_1: 1;

            then (rseq . n) in ( rng rseq) by FUNCT_1:def 3;

            then

             A7: (( sec | [. 0 , ( PI / 2).[) . (rseq . n)) = ( sec . (rseq . n)) by A4, A6, FUNCT_1: 49;

            (( sec | [. 0 , ( PI / 2).[) . (rseq . n)) = ((( sec | [. 0 , ( PI / 2).[) /* rseq) . n) by A4, FUNCT_2: 108;

            hence ((( sec | [. 0 , ( PI / 2).[) /* rseq) . n) = (( sec /* rseq) . n) by A4, A6, A7, Th1, FUNCT_2: 108, XBOOLE_1: 1;

          end;

          then

           A8: (( sec | [. 0 , ( PI / 2).[) /* rseq) = ( sec /* rseq) by FUNCT_2: 63;

          

           A9: ( rng rseq) c= ( dom sec ) by A4, A6, Th1;

          then ( sec . th) = ( lim ( sec /* rseq)) by A3, A5, FCONT_1:def 1;

          hence (( sec | [. 0 , ( PI / 2).[) /* rseq) is convergent & (( sec | [. 0 , ( PI / 2).[) . th) = ( lim (( sec | [. 0 , ( PI / 2).[) /* rseq)) by A2, A3, A5, A9, A8, Lm33, FCONT_1:def 1;

        end;

        hence thesis by FCONT_1:def 1;

      end;

      hence thesis by FCONT_1:def 2;

    end;

    theorem :: SINCOS10:38

    

     Th38: ( sec | ].( PI / 2), PI .]) is continuous

    proof

      for th be Real st th in ( dom ( sec | ].( PI / 2), PI .])) holds ( sec | ].( PI / 2), PI .]) is_continuous_in th

      proof

        let th be Real;

        

         A1: cos is_differentiable_in th by SIN_COS: 63;

        assume

         A2: th in ( dom ( sec | ].( PI / 2), PI .]));

        then th in ].( PI / 2), PI .] by RELAT_1: 57;

        then ( cos . th) <> 0 by Lm2, COMPTRIG: 13;

        then

         A3: sec is_continuous_in th by A1, FCONT_1: 10, FDIFF_1: 24;

        now

          let rseq;

          assume that

           A4: ( rng rseq) c= ( dom ( sec | ].( PI / 2), PI .])) and

           A5: rseq is convergent & ( lim rseq) = th;

          

           A6: ( dom ( sec | ].( PI / 2), PI .])) = ].( PI / 2), PI .] by Th2, RELAT_1: 62;

          now

            let n be Element of NAT ;

            ( dom rseq) = NAT by SEQ_1: 1;

            then (rseq . n) in ( rng rseq) by FUNCT_1:def 3;

            then

             A7: (( sec | ].( PI / 2), PI .]) . (rseq . n)) = ( sec . (rseq . n)) by A4, A6, FUNCT_1: 49;

            (( sec | ].( PI / 2), PI .]) . (rseq . n)) = ((( sec | ].( PI / 2), PI .]) /* rseq) . n) by A4, FUNCT_2: 108;

            hence ((( sec | ].( PI / 2), PI .]) /* rseq) . n) = (( sec /* rseq) . n) by A4, A6, A7, Th2, FUNCT_2: 108, XBOOLE_1: 1;

          end;

          then

           A8: (( sec | ].( PI / 2), PI .]) /* rseq) = ( sec /* rseq) by FUNCT_2: 63;

          

           A9: ( rng rseq) c= ( dom sec ) by A4, A6, Th2;

          then ( sec . th) = ( lim ( sec /* rseq)) by A3, A5, FCONT_1:def 1;

          hence (( sec | ].( PI / 2), PI .]) /* rseq) is convergent & (( sec | ].( PI / 2), PI .]) . th) = ( lim (( sec | ].( PI / 2), PI .]) /* rseq)) by A2, A3, A5, A9, A8, Lm34, FCONT_1:def 1;

        end;

        hence thesis by FCONT_1:def 1;

      end;

      hence thesis by FCONT_1:def 2;

    end;

    theorem :: SINCOS10:39

    

     Th39: ( cosec | [.( - ( PI / 2)), 0 .[) is continuous

    proof

      for th be Real st th in ( dom ( cosec | [.( - ( PI / 2)), 0 .[)) holds ( cosec | [.( - ( PI / 2)), 0 .[) is_continuous_in th

      proof

        let th be Real;

        assume

         A1: th in ( dom ( cosec | [.( - ( PI / 2)), 0 .[));

        then

         A2: th in [.( - ( PI / 2)), 0 .[ by RELAT_1: 57;

        then th < 0 by Lm3, XXREAL_1: 4;

        then

         A3: (th + (2 * PI )) < ( 0 + (2 * PI )) by XREAL_1: 8;

        ( - PI ) < th by A2, Lm3, XXREAL_1: 4;

        then (( - PI ) + (2 * PI )) < (th + (2 * PI )) by XREAL_1: 8;

        then (th + (2 * PI )) in ]. PI , (2 * PI ).[ by A3;

        then ( sin . (th + (2 * PI ))) <> 0 by COMPTRIG: 9;

        then

         A4: ( sin . th) <> 0 by SIN_COS: 78;

         sin is_differentiable_in th by SIN_COS: 64;

        then

         A5: cosec is_continuous_in th by A4, FCONT_1: 10, FDIFF_1: 24;

        now

          let rseq;

          assume that

           A6: ( rng rseq) c= ( dom ( cosec | [.( - ( PI / 2)), 0 .[)) and

           A7: rseq is convergent & ( lim rseq) = th;

          

           A8: ( dom ( cosec | [.( - ( PI / 2)), 0 .[)) = [.( - ( PI / 2)), 0 .[ by Th3, RELAT_1: 62;

          now

            let n be Element of NAT ;

            ( dom rseq) = NAT by SEQ_1: 1;

            then (rseq . n) in ( rng rseq) by FUNCT_1:def 3;

            then

             A9: (( cosec | [.( - ( PI / 2)), 0 .[) . (rseq . n)) = ( cosec . (rseq . n)) by A6, A8, FUNCT_1: 49;

            (( cosec | [.( - ( PI / 2)), 0 .[) . (rseq . n)) = ((( cosec | [.( - ( PI / 2)), 0 .[) /* rseq) . n) by A6, FUNCT_2: 108;

            hence ((( cosec | [.( - ( PI / 2)), 0 .[) /* rseq) . n) = (( cosec /* rseq) . n) by A6, A8, A9, Th3, FUNCT_2: 108, XBOOLE_1: 1;

          end;

          then

           A10: (( cosec | [.( - ( PI / 2)), 0 .[) /* rseq) = ( cosec /* rseq) by FUNCT_2: 63;

          

           A11: ( rng rseq) c= ( dom cosec ) by A6, A8, Th3;

          then ( cosec . th) = ( lim ( cosec /* rseq)) by A5, A7, FCONT_1:def 1;

          hence (( cosec | [.( - ( PI / 2)), 0 .[) /* rseq) is convergent & (( cosec | [.( - ( PI / 2)), 0 .[) . th) = ( lim (( cosec | [.( - ( PI / 2)), 0 .[) /* rseq)) by A1, A5, A7, A11, A10, Lm35, FCONT_1:def 1;

        end;

        hence thesis by FCONT_1:def 1;

      end;

      hence thesis by FCONT_1:def 2;

    end;

    theorem :: SINCOS10:40

    

     Th40: ( cosec | ]. 0 , ( PI / 2).]) is continuous

    proof

      for th be Real st th in ( dom ( cosec | ]. 0 , ( PI / 2).])) holds ( cosec | ]. 0 , ( PI / 2).]) is_continuous_in th

      proof

        let th be Real;

        

         A1: sin is_differentiable_in th by SIN_COS: 64;

        assume

         A2: th in ( dom ( cosec | ]. 0 , ( PI / 2).]));

        then th in ]. 0 , ( PI / 2).] by RELAT_1: 57;

        then ( sin . th) <> 0 by Lm4, COMPTRIG: 7;

        then

         A3: cosec is_continuous_in th by A1, FCONT_1: 10, FDIFF_1: 24;

        now

          let rseq;

          assume that

           A4: ( rng rseq) c= ( dom ( cosec | ]. 0 , ( PI / 2).])) and

           A5: rseq is convergent & ( lim rseq) = th;

          

           A6: ( dom ( cosec | ]. 0 , ( PI / 2).])) = ]. 0 , ( PI / 2).] by Th4, RELAT_1: 62;

          now

            let n be Element of NAT ;

            ( dom rseq) = NAT by SEQ_1: 1;

            then (rseq . n) in ( rng rseq) by FUNCT_1:def 3;

            then

             A7: (( cosec | ]. 0 , ( PI / 2).]) . (rseq . n)) = ( cosec . (rseq . n)) by A4, A6, FUNCT_1: 49;

            (( cosec | ]. 0 , ( PI / 2).]) . (rseq . n)) = ((( cosec | ]. 0 , ( PI / 2).]) /* rseq) . n) by A4, FUNCT_2: 108;

            hence ((( cosec | ]. 0 , ( PI / 2).]) /* rseq) . n) = (( cosec /* rseq) . n) by A4, A6, A7, Th4, FUNCT_2: 108, XBOOLE_1: 1;

          end;

          then

           A8: (( cosec | ]. 0 , ( PI / 2).]) /* rseq) = ( cosec /* rseq) by FUNCT_2: 63;

          

           A9: ( rng rseq) c= ( dom cosec ) by A4, A6, Th4;

          then ( cosec . th) = ( lim ( cosec /* rseq)) by A3, A5, FCONT_1:def 1;

          hence (( cosec | ]. 0 , ( PI / 2).]) /* rseq) is convergent & (( cosec | ]. 0 , ( PI / 2).]) . th) = ( lim (( cosec | ]. 0 , ( PI / 2).]) /* rseq)) by A2, A3, A5, A9, A8, Lm36, FCONT_1:def 1;

        end;

        hence thesis by FCONT_1:def 1;

      end;

      hence thesis by FCONT_1:def 2;

    end;

    theorem :: SINCOS10:41

    

     Th41: ( rng ( sec | [. 0 , ( PI / 4).])) = [.1, ( sqrt 2).]

    proof

      now

        let y be object;

        thus y in [.1, ( sqrt 2).] implies ex x be object st x in ( dom ( sec | [. 0 , ( PI / 4).])) & y = (( sec | [. 0 , ( PI / 4).]) . x)

        proof

          assume

           A1: y in [.1, ( sqrt 2).];

          then

          reconsider y1 = y as Real;

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

          then

           A2: ( sec | [. 0 , ( PI / 4).]) is continuous by Th37, FCONT_1: 16;

          y1 in ( [.( sec . 0 ), ( sec . ( PI / 4)).] \/ [.( sec . ( PI / 4)), ( sec . 0 ).]) by A1, Th31, XBOOLE_0:def 3;

          then

          consider x be Real such that

           A3: x in [. 0 , ( PI / 4).] & y1 = ( sec . x) by A2, Lm13, Th1, FCONT_2: 15, XBOOLE_1: 1;

          take x;

          thus thesis by A3, Lm29, FUNCT_1: 49;

        end;

        thus (ex x be object st x in ( dom ( sec | [. 0 , ( PI / 4).])) & y = (( sec | [. 0 , ( PI / 4).]) . x)) implies y in [.1, ( sqrt 2).]

        proof

          given x be object such that

           A4: x in ( dom ( sec | [. 0 , ( PI / 4).])) and

           A5: y = (( sec | [. 0 , ( PI / 4).]) . x);

          reconsider x1 = x as Real by A4;

          y = ( sec . x1) by A4, A5, Lm29, FUNCT_1: 49;

          hence thesis by A4, Lm29, Th33;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: SINCOS10:42

    

     Th42: ( rng ( sec | [.((3 / 4) * PI ), PI .])) = [.( - ( sqrt 2)), ( - 1).]

    proof

      now

        let y be object;

        thus y in [.( - ( sqrt 2)), ( - 1).] implies ex x be object st x in ( dom ( sec | [.((3 / 4) * PI ), PI .])) & y = (( sec | [.((3 / 4) * PI ), PI .]) . x)

        proof

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

          then

           A1: ( sec | [.((3 / 4) * PI ), PI .]) is continuous by Th38, FCONT_1: 16;

          assume

           A2: y in [.( - ( sqrt 2)), ( - 1).];

          then

          reconsider y1 = y as Real;

          

           A3: ((3 / 4) * PI ) <= PI by Lm6, XXREAL_1: 2;

          y1 in ( [.( sec . ((3 / 4) * PI )), ( sec . PI ).] \/ [.( sec . PI ), ( sec . ((3 / 4) * PI )).]) by A2, Th31, XBOOLE_0:def 3;

          then

          consider x be Real such that

           A4: x in [.((3 / 4) * PI ), PI .] & y1 = ( sec . x) by A3, A1, Lm14, Th2, FCONT_2: 15, XBOOLE_1: 1;

          take x;

          thus thesis by A4, Lm30, FUNCT_1: 49;

        end;

        thus (ex x be object 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 object such that

           A5: x in ( dom ( sec | [.((3 / 4) * PI ), PI .])) and

           A6: y = (( sec | [.((3 / 4) * PI ), PI .]) . x);

          reconsider x1 = x as Real by A5;

          y = ( sec . x1) by A5, A6, Lm30, FUNCT_1: 49;

          hence thesis by A5, Lm30, Th34;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: SINCOS10:43

    

     Th43: ( rng ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).])) = [.( - ( sqrt 2)), ( - 1).]

    proof

      now

        let y be object;

        thus y in [.( - ( sqrt 2)), ( - 1).] implies ex x be object st x in ( dom ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).])) & y = (( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) . x)

        proof

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

          then

           A1: ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) is continuous by Th39, FCONT_1: 16;

          assume

           A2: y in [.( - ( sqrt 2)), ( - 1).];

          then

          reconsider y1 = y as Real;

          

           A3: ( - ( PI / 2)) <= ( - ( PI / 4)) by Lm7, XXREAL_1: 3;

          y1 in ( [.( cosec . ( - ( PI / 4))), ( cosec . ( - ( PI / 2))).] \/ [.( cosec . ( - ( PI / 2))), ( cosec . ( - ( PI / 4))).]) by A2, Th32, XBOOLE_0:def 3;

          then

          consider x be Real such that

           A4: x in [.( - ( PI / 2)), ( - ( PI / 4)).] & y1 = ( cosec . x) by A3, A1, Lm19, Th3, FCONT_2: 15, XBOOLE_1: 1;

          take x;

          thus thesis by A4, Lm31, FUNCT_1: 49;

        end;

        thus (ex x be object 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 object such that

           A5: x in ( dom ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).])) and

           A6: y = (( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) . x);

          reconsider x1 = x as Real by A5;

          y = ( cosec . x1) by A5, A6, Lm31, FUNCT_1: 49;

          hence thesis by A5, Lm31, Th35;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: SINCOS10:44

    

     Th44: ( rng ( cosec | [.( PI / 4), ( PI / 2).])) = [.1, ( sqrt 2).]

    proof

      now

        let y be object;

        thus y in [.1, ( sqrt 2).] implies ex x be object st x in ( dom ( cosec | [.( PI / 4), ( PI / 2).])) & y = (( cosec | [.( PI / 4), ( PI / 2).]) . x)

        proof

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

          then

           A1: ( cosec | [.( PI / 4), ( PI / 2).]) is continuous by Th40, FCONT_1: 16;

          assume

           A2: y in [.1, ( sqrt 2).];

          then

          reconsider y1 = y as Real;

          

           A3: ( PI / 4) <= ( PI / 2) by Lm8, XXREAL_1: 2;

          y1 in ( [.( cosec . ( PI / 2)), ( cosec . ( PI / 4)).] \/ [.( cosec . ( PI / 4)), ( cosec . ( PI / 2)).]) by A2, Th32, XBOOLE_0:def 3;

          then

          consider x be Real such that

           A4: x in [.( PI / 4), ( PI / 2).] & y1 = ( cosec . x) by A3, A1, Lm20, Th4, FCONT_2: 15, XBOOLE_1: 1;

          take x;

          thus thesis by A4, Lm32, FUNCT_1: 49;

        end;

        thus (ex x be object 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 object such that

           A5: x in ( dom ( cosec | [.( PI / 4), ( PI / 2).])) and

           A6: y = (( cosec | [.( PI / 4), ( PI / 2).]) . x);

          reconsider x1 = x as Real by A5;

          y = ( cosec . x1) by A5, A6, Lm32, FUNCT_1: 49;

          hence thesis by A5, Lm32, Th36;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: SINCOS10:45

    

     Th45: [.1, ( sqrt 2).] c= ( dom arcsec1 )

    proof

      

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

      ( rng ( sec | [. 0 , ( PI / 4).])) c= ( rng ( sec | [. 0 , ( PI / 2).[))

      proof

        let y be object;

        assume y in ( rng ( sec | [. 0 , ( PI / 4).]));

        then y in ( sec .: [. 0 , ( PI / 4).]) by RELAT_1: 115;

        then ex x be object st x in ( dom sec ) & x in [. 0 , ( PI / 4).] & y = ( sec . x) by FUNCT_1:def 6;

        then y in ( sec .: [. 0 , ( PI / 2).[) by A1, FUNCT_1:def 6;

        hence thesis by RELAT_1: 115;

      end;

      hence thesis by Th41, FUNCT_1: 33;

    end;

    theorem :: SINCOS10:46

    

     Th46: [.( - ( sqrt 2)), ( - 1).] c= ( dom arcsec2 )

    proof

      

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

      ( rng ( sec | [.((3 / 4) * PI ), PI .])) c= ( rng ( sec | ].( PI / 2), PI .]))

      proof

        let y be object;

        assume y in ( rng ( sec | [.((3 / 4) * PI ), PI .]));

        then y in ( sec .: [.((3 / 4) * PI ), PI .]) by RELAT_1: 115;

        then ex x be object st x in ( dom sec ) & x in [.((3 / 4) * PI ), PI .] & y = ( sec . x) by FUNCT_1:def 6;

        then y in ( sec .: ].( PI / 2), PI .]) by A1, FUNCT_1:def 6;

        hence thesis by RELAT_1: 115;

      end;

      hence thesis by Th42, FUNCT_1: 33;

    end;

    theorem :: SINCOS10:47

    

     Th47: [.( - ( sqrt 2)), ( - 1).] c= ( dom arccosec1 )

    proof

      

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

      ( rng ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).])) c= ( rng ( cosec | [.( - ( PI / 2)), 0 .[))

      proof

        let y be object;

        assume y in ( rng ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]));

        then y in ( cosec .: [.( - ( PI / 2)), ( - ( PI / 4)).]) by RELAT_1: 115;

        then ex x be object st x in ( dom cosec ) & x in [.( - ( PI / 2)), ( - ( PI / 4)).] & y = ( cosec . x) by FUNCT_1:def 6;

        then y in ( cosec .: [.( - ( PI / 2)), 0 .[) by A1, FUNCT_1:def 6;

        hence thesis by RELAT_1: 115;

      end;

      hence thesis by Th43, FUNCT_1: 33;

    end;

    theorem :: SINCOS10:48

    

     Th48: [.1, ( sqrt 2).] c= ( dom arccosec2 )

    proof

      

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

      ( rng ( cosec | [.( PI / 4), ( PI / 2).])) c= ( rng ( cosec | ]. 0 , ( PI / 2).]))

      proof

        let y be object;

        assume y in ( rng ( cosec | [.( PI / 4), ( PI / 2).]));

        then y in ( cosec .: [.( PI / 4), ( PI / 2).]) by RELAT_1: 115;

        then ex x be object st x in ( dom cosec ) & x in [.( PI / 4), ( PI / 2).] & y = ( cosec . x) by FUNCT_1:def 6;

        then y in ( cosec .: ]. 0 , ( PI / 2).]) by A1, FUNCT_1:def 6;

        hence thesis by RELAT_1: 115;

      end;

      hence thesis by Th44, FUNCT_1: 33;

    end;

    

     Lm37: (( sec | [. 0 , ( PI / 4).]) | [. 0 , ( PI / 4).]) is increasing

    proof

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

      then ( sec | [. 0 , ( PI / 4).]) is increasing by Th17, RFUNCT_2: 28;

      hence thesis;

    end;

    

     Lm38: (( sec | [.((3 / 4) * PI ), PI .]) | [.((3 / 4) * PI ), PI .]) is increasing

    proof

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

      then ( sec | [.((3 / 4) * PI ), PI .]) is increasing by Th18, RFUNCT_2: 28;

      hence thesis;

    end;

    

     Lm39: (( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) | [.( - ( PI / 2)), ( - ( PI / 4)).]) is decreasing

    proof

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

      then ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) is decreasing by Th19, RFUNCT_2: 29;

      hence thesis;

    end;

    

     Lm40: (( cosec | [.( PI / 4), ( PI / 2).]) | [.( PI / 4), ( PI / 2).]) is decreasing

    proof

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

      then ( cosec | [.( PI / 4), ( PI / 2).]) is decreasing by Th20, RFUNCT_2: 29;

      hence thesis;

    end;

    

     Lm41: ( sec | [. 0 , ( PI / 4).]) is one-to-one

    proof

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

      then (( sec | [. 0 , ( PI / 2).[) | [. 0 , ( PI / 4).]) = ( sec | [. 0 , ( PI / 4).]) by RELAT_1: 74;

      hence thesis;

    end;

    

     Lm42: ( sec | [.((3 / 4) * PI ), PI .]) is one-to-one

    proof

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

      then (( sec | ].( PI / 2), PI .]) | [.((3 / 4) * PI ), PI .]) = ( sec | [.((3 / 4) * PI ), PI .]) by RELAT_1: 74;

      hence thesis;

    end;

    

     Lm43: ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) is one-to-one

    proof

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

      then (( cosec | [.( - ( PI / 2)), 0 .[) | [.( - ( PI / 2)), ( - ( PI / 4)).]) = ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) by RELAT_1: 74;

      hence thesis;

    end;

    

     Lm44: ( cosec | [.( PI / 4), ( PI / 2).]) is one-to-one

    proof

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

      then (( cosec | ]. 0 , ( PI / 2).]) | [.( PI / 4), ( PI / 2).]) = ( cosec | [.( PI / 4), ( PI / 2).]) by RELAT_1: 74;

      hence thesis;

    end;

    registration

      cluster ( sec | [. 0 , ( PI / 4).]) -> one-to-one;

      coherence by Lm41;

      cluster ( sec | [.((3 / 4) * PI ), PI .]) -> one-to-one;

      coherence by Lm42;

      cluster ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) -> one-to-one;

      coherence by Lm43;

      cluster ( cosec | [.( PI / 4), ( PI / 2).]) -> one-to-one;

      coherence by Lm44;

    end

    theorem :: SINCOS10:49

    

     Th49: ( arcsec1 | [.1, ( sqrt 2).]) = (( sec | [. 0 , ( PI / 4).]) " )

    proof

      set h = ( sec | [. 0 , ( PI / 2).[);

      

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

      

      then (( sec | [. 0 , ( PI / 4).]) " ) = ((h | [. 0 , ( PI / 4).]) " ) by RELAT_1: 74

      .= ((h " ) | (h .: [. 0 , ( PI / 4).])) by RFUNCT_2: 17

      .= ((h " ) | ( rng (h | [. 0 , ( PI / 4).]))) by RELAT_1: 115

      .= ((h " ) | [.1, ( sqrt 2).]) by A1, Th41, RELAT_1: 74;

      hence thesis;

    end;

    theorem :: SINCOS10:50

    

     Th50: ( arcsec2 | [.( - ( sqrt 2)), ( - 1).]) = (( sec | [.((3 / 4) * PI ), PI .]) " )

    proof

      set h = ( sec | ].( PI / 2), PI .]);

      

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

      

      then (( sec | [.((3 / 4) * PI ), PI .]) " ) = ((h | [.((3 / 4) * PI ), PI .]) " ) by RELAT_1: 74

      .= ((h " ) | (h .: [.((3 / 4) * PI ), PI .])) by RFUNCT_2: 17

      .= ((h " ) | ( rng (h | [.((3 / 4) * PI ), PI .]))) by RELAT_1: 115

      .= ((h " ) | [.( - ( sqrt 2)), ( - 1).]) by A1, Th42, RELAT_1: 74;

      hence thesis;

    end;

    theorem :: SINCOS10:51

    

     Th51: ( arccosec1 | [.( - ( sqrt 2)), ( - 1).]) = (( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) " )

    proof

      set h = ( cosec | [.( - ( PI / 2)), 0 .[);

      

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

      

      then (( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) " ) = ((h | [.( - ( PI / 2)), ( - ( PI / 4)).]) " ) by RELAT_1: 74

      .= ((h " ) | (h .: [.( - ( PI / 2)), ( - ( PI / 4)).])) by RFUNCT_2: 17

      .= ((h " ) | ( rng (h | [.( - ( PI / 2)), ( - ( PI / 4)).]))) by RELAT_1: 115

      .= ((h " ) | [.( - ( sqrt 2)), ( - 1).]) by A1, Th43, RELAT_1: 74;

      hence thesis;

    end;

    theorem :: SINCOS10:52

    

     Th52: ( arccosec2 | [.1, ( sqrt 2).]) = (( cosec | [.( PI / 4), ( PI / 2).]) " )

    proof

      set h = ( cosec | ]. 0 , ( PI / 2).]);

      

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

      

      then (( cosec | [.( PI / 4), ( PI / 2).]) " ) = ((h | [.( PI / 4), ( PI / 2).]) " ) by RELAT_1: 74

      .= ((h " ) | (h .: [.( PI / 4), ( PI / 2).])) by RFUNCT_2: 17

      .= ((h " ) | ( rng (h | [.( PI / 4), ( PI / 2).]))) by RELAT_1: 115

      .= ((h " ) | [.1, ( sqrt 2).]) by A1, Th44, RELAT_1: 74;

      hence thesis;

    end;

    theorem :: SINCOS10:53

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

    theorem :: SINCOS10:54

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

    theorem :: SINCOS10:55

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

    theorem :: SINCOS10:56

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

    theorem :: SINCOS10:57

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

    theorem :: SINCOS10:58

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

    theorem :: SINCOS10:59

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

    theorem :: SINCOS10:60

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

    theorem :: SINCOS10:61

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

    theorem :: SINCOS10:62

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

    theorem :: SINCOS10:63

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

    theorem :: SINCOS10:64

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

    theorem :: SINCOS10:65

    

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

    theorem :: SINCOS10:66

    

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

    theorem :: SINCOS10:67

    

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

    theorem :: SINCOS10:68

    

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

    theorem :: SINCOS10:69

    

     Th69: 0 <= r & r < ( PI / 2) implies ( arcsec1 ( sec . r)) = r

    proof

      

       A1: ( dom ( sec | [. 0 , ( PI / 2).[)) = [. 0 , ( PI / 2).[ by Th1, RELAT_1: 62;

      assume 0 <= r & r < ( PI / 2);

      then

       A2: r in [. 0 , ( PI / 2).[;

      

      then ( arcsec1 ( sec . r)) = ( arcsec1 . (( sec | [. 0 , ( PI / 2).[) . r)) by FUNCT_1: 49

      .= (( id [. 0 , ( PI / 2).[) . r) by A2, A1, Th65, FUNCT_1: 13

      .= r by A2, FUNCT_1: 18;

      hence thesis;

    end;

    theorem :: SINCOS10:70

    

     Th70: ( PI / 2) < r & r <= PI implies ( arcsec2 ( sec . r)) = r

    proof

      

       A1: ( dom ( sec | ].( PI / 2), PI .])) = ].( PI / 2), PI .] by Th2, RELAT_1: 62;

      assume ( PI / 2) < r & r <= PI ;

      then

       A2: r in ].( PI / 2), PI .];

      

      then ( arcsec2 ( sec . r)) = ( arcsec2 . (( sec | ].( PI / 2), PI .]) . r)) by FUNCT_1: 49

      .= (( id ].( PI / 2), PI .]) . r) by A2, A1, Th66, FUNCT_1: 13

      .= r by A2, FUNCT_1: 18;

      hence thesis;

    end;

    theorem :: SINCOS10:71

    

     Th71: ( - ( PI / 2)) <= r & r < 0 implies ( arccosec1 ( cosec . r)) = r

    proof

      

       A1: ( dom ( cosec | [.( - ( PI / 2)), 0 .[)) = [.( - ( PI / 2)), 0 .[ by Th3, RELAT_1: 62;

      assume ( - ( PI / 2)) <= r & r < 0 ;

      then

       A2: r in [.( - ( PI / 2)), 0 .[;

      

      then ( arccosec1 ( cosec . r)) = ( arccosec1 . (( cosec | [.( - ( PI / 2)), 0 .[) . r)) by FUNCT_1: 49

      .= (( id [.( - ( PI / 2)), 0 .[) . r) by A2, A1, Th67, FUNCT_1: 13

      .= r by A2, FUNCT_1: 18;

      hence thesis;

    end;

    theorem :: SINCOS10:72

    

     Th72: 0 < r & r <= ( PI / 2) implies ( arccosec2 ( cosec . r)) = r

    proof

      

       A1: ( dom ( cosec | ]. 0 , ( PI / 2).])) = ]. 0 , ( PI / 2).] by Th4, RELAT_1: 62;

      assume 0 < r & r <= ( PI / 2);

      then

       A2: r in ]. 0 , ( PI / 2).];

      

      then ( arccosec2 ( cosec . r)) = ( arccosec2 . (( cosec | ]. 0 , ( PI / 2).]) . r)) by FUNCT_1: 49

      .= (( id ]. 0 , ( PI / 2).]) . r) by A2, A1, Th68, FUNCT_1: 13

      .= r by A2, FUNCT_1: 18;

      hence thesis;

    end;

    theorem :: SINCOS10:73

    

     Th73: ( arcsec1 . 1) = 0 & ( arcsec1 . ( sqrt 2)) = ( PI / 4)

    proof

      

       A1: ( arcsec1 . 1) = ( arcsec1 1)

      .= 0 by Th31, Th69;

      

       A2: ( PI / 4) < ( PI / 2) by Lm5, XXREAL_1: 3;

      ( arcsec1 . ( sqrt 2)) = ( arcsec1 ( sqrt 2))

      .= ( PI / 4) by A2, Th31, Th69;

      hence thesis by A1;

    end;

    theorem :: SINCOS10:74

    

     Th74: ( arcsec2 . ( - ( sqrt 2))) = ((3 / 4) * PI ) & ( arcsec2 . ( - 1)) = PI

    proof

      

       A1: ( PI / 2) < PI by Lm6, XXREAL_1: 2;

      

       A2: ( arcsec2 . ( - 1)) = ( arcsec2 ( - 1))

      .= PI by A1, Th31, Th70;

      

       A3: ( PI / 2) < ((3 / 4) * PI ) & ((3 / 4) * PI ) <= PI by Lm6, XXREAL_1: 2;

      ( arcsec2 . ( - ( sqrt 2))) = ( arcsec2 ( - ( sqrt 2)))

      .= ((3 / 4) * PI ) by A3, Th31, Th70;

      hence thesis by A2;

    end;

    theorem :: SINCOS10:75

    

     Th75: ( arccosec1 . ( - 1)) = ( - ( PI / 2)) & ( arccosec1 . ( - ( sqrt 2))) = ( - ( PI / 4))

    proof

      

       A1: ( arccosec1 . ( - 1)) = ( arccosec1 ( - 1))

      .= ( - ( PI / 2)) by Th32, Th71;

      

       A2: ( - ( PI / 2)) <= ( - ( PI / 4)) by Lm7, XXREAL_1: 3;

      ( arccosec1 . ( - ( sqrt 2))) = ( arccosec1 ( - ( sqrt 2)))

      .= ( - ( PI / 4)) by A2, Th32, Th71;

      hence thesis by A1;

    end;

    theorem :: SINCOS10:76

    

     Th76: ( arccosec2 . ( sqrt 2)) = ( PI / 4) & ( arccosec2 . 1) = ( PI / 2)

    proof

      

       A1: ( arccosec2 . 1) = ( arccosec2 1)

      .= ( PI / 2) by Th32, Th72;

      

       A2: ( PI / 4) <= ( PI / 2) by Lm8, XXREAL_1: 2;

      ( arccosec2 . ( sqrt 2)) = ( arccosec2 ( sqrt 2))

      .= ( PI / 4) by A2, Th32, Th72;

      hence thesis by A1;

    end;

    theorem :: SINCOS10:77

    

     Th77: ( arcsec1 | ( sec .: [. 0 , ( PI / 2).[)) is increasing

    proof

      set f = ( sec | [. 0 , ( PI / 2).[);

      

       A1: (f .: [. 0 , ( PI / 2).[) = ( rng (f | [. 0 , ( PI / 2).[)) by RELAT_1: 115

      .= ( rng ( sec | [. 0 , ( PI / 2).[)) by RELAT_1: 73

      .= ( sec .: [. 0 , ( PI / 2).[) by RELAT_1: 115;

      (f | [. 0 , ( PI / 2).[) = f by RELAT_1: 73;

      hence thesis by A1, Th17, FCONT_3: 9;

    end;

    theorem :: SINCOS10:78

    

     Th78: ( arcsec2 | ( sec .: ].( PI / 2), PI .])) is increasing

    proof

      set f = ( sec | ].( PI / 2), PI .]);

      

       A1: (f .: ].( PI / 2), PI .]) = ( rng (f | ].( PI / 2), PI .])) by RELAT_1: 115

      .= ( rng ( sec | ].( PI / 2), PI .])) by RELAT_1: 73

      .= ( sec .: ].( PI / 2), PI .]) by RELAT_1: 115;

      (f | ].( PI / 2), PI .]) = f by RELAT_1: 73;

      hence thesis by A1, Th18, FCONT_3: 9;

    end;

    theorem :: SINCOS10:79

    

     Th79: ( arccosec1 | ( cosec .: [.( - ( PI / 2)), 0 .[)) is decreasing

    proof

      set f = ( cosec | [.( - ( PI / 2)), 0 .[);

      

       A1: (f .: [.( - ( PI / 2)), 0 .[) = ( rng (f | [.( - ( PI / 2)), 0 .[)) by RELAT_1: 115

      .= ( rng ( cosec | [.( - ( PI / 2)), 0 .[)) by RELAT_1: 73

      .= ( cosec .: [.( - ( PI / 2)), 0 .[) by RELAT_1: 115;

      (f | [.( - ( PI / 2)), 0 .[) = f by RELAT_1: 73;

      hence thesis by A1, Th19, FCONT_3: 10;

    end;

    theorem :: SINCOS10:80

    

     Th80: ( arccosec2 | ( cosec .: ]. 0 , ( PI / 2).])) is decreasing

    proof

      set f = ( cosec | ]. 0 , ( PI / 2).]);

      

       A1: (f .: ]. 0 , ( PI / 2).]) = ( rng (f | ]. 0 , ( PI / 2).])) by RELAT_1: 115

      .= ( rng ( cosec | ]. 0 , ( PI / 2).])) by RELAT_1: 73

      .= ( cosec .: ]. 0 , ( PI / 2).]) by RELAT_1: 115;

      (f | ]. 0 , ( PI / 2).]) = f by RELAT_1: 73;

      hence thesis by A1, Th20, FCONT_3: 10;

    end;

    theorem :: SINCOS10:81

    

     Th81: ( arcsec1 | [.1, ( sqrt 2).]) is increasing

    proof

       [.1, ( sqrt 2).] = ( sec .: [. 0 , ( PI / 4).]) & [. 0 , ( PI / 4).] c= [. 0 , ( PI / 2).[ by Lm5, Th41, RELAT_1: 115, XXREAL_2:def 12;

      hence thesis by Th77, RELAT_1: 123, RFUNCT_2: 28;

    end;

    theorem :: SINCOS10:82

    

     Th82: ( arcsec2 | [.( - ( sqrt 2)), ( - 1).]) is increasing

    proof

       [.( - ( sqrt 2)), ( - 1).] = ( sec .: [.((3 / 4) * PI ), PI .]) & [.((3 / 4) * PI ), PI .] c= ].( PI / 2), PI .] by Lm6, Th42, RELAT_1: 115, XXREAL_2:def 12;

      hence thesis by Th78, RELAT_1: 123, RFUNCT_2: 28;

    end;

    theorem :: SINCOS10:83

    

     Th83: ( arccosec1 | [.( - ( sqrt 2)), ( - 1).]) is decreasing

    proof

       [.( - ( sqrt 2)), ( - 1).] = ( cosec .: [.( - ( PI / 2)), ( - ( PI / 4)).]) & [.( - ( PI / 2)), ( - ( PI / 4)).] c= [.( - ( PI / 2)), 0 .[ by Lm7, Th43, RELAT_1: 115, XXREAL_2:def 12;

      hence thesis by Th79, RELAT_1: 123, RFUNCT_2: 29;

    end;

    theorem :: SINCOS10:84

    

     Th84: ( arccosec2 | [.1, ( sqrt 2).]) is decreasing

    proof

       [.1, ( sqrt 2).] = ( cosec .: [.( PI / 4), ( PI / 2).]) & [.( PI / 4), ( PI / 2).] c= ]. 0 , ( PI / 2).] by Lm8, Th44, RELAT_1: 115, XXREAL_2:def 12;

      hence thesis by Th80, RELAT_1: 123, RFUNCT_2: 29;

    end;

    theorem :: SINCOS10:85

    

     Th85: for x be set st x in [.1, ( sqrt 2).] holds ( arcsec1 . x) in [. 0 , ( PI / 4).]

    proof

      let x be set;

      assume x in [.1, ( sqrt 2).];

      then x in ( ].1, ( sqrt 2).[ \/ {1, ( sqrt 2)}) by SQUARE_1: 19, XXREAL_1: 128;

      then

       A1: x in ].1, ( sqrt 2).[ or x in {1, ( sqrt 2)} by XBOOLE_0:def 3;

      per cases by A1, TARSKI:def 2;

        suppose

         A2: x in ].1, ( sqrt 2).[;

        then

         A3: ].1, ( sqrt 2).[ c= [.1, ( sqrt 2).] & ex s be Real st s = x & 1 < s & s < ( sqrt 2) by XXREAL_1: 25;

        

         A4: ( [.1, ( sqrt 2).] /\ ( dom arcsec1 )) = [.1, ( sqrt 2).] by Th45, XBOOLE_1: 28;

        then ( sqrt 2) in ( [.1, ( sqrt 2).] /\ ( dom arcsec1 )) by SQUARE_1: 19;

        then

         A5: ( arcsec1 . x) < ( PI / 4) by A2, A4, A3, Th73, Th81, RFUNCT_2: 20;

        1 in [.1, ( sqrt 2).] by SQUARE_1: 19;

        then 0 < ( arcsec1 . x) by A2, A4, A3, Th73, Th81, RFUNCT_2: 20;

        hence thesis by A5;

      end;

        suppose x = 1;

        hence thesis by Th73;

      end;

        suppose x = ( sqrt 2);

        hence thesis by Th73;

      end;

    end;

    theorem :: SINCOS10:86

    

     Th86: for x be set st x in [.( - ( sqrt 2)), ( - 1).] holds ( arcsec2 . x) in [.((3 / 4) * PI ), PI .]

    proof

      let x be set;

      

       A1: ( - ( sqrt 2)) < ( - 1) by SQUARE_1: 19, XREAL_1: 24;

      assume x in [.( - ( sqrt 2)), ( - 1).];

      then x in ( ].( - ( sqrt 2)), ( - 1).[ \/ {( - ( sqrt 2)), ( - 1)}) by A1, XXREAL_1: 128;

      then

       A2: x in ].( - ( sqrt 2)), ( - 1).[ or x in {( - ( sqrt 2)), ( - 1)} by XBOOLE_0:def 3;

      per cases by A2, TARSKI:def 2;

        suppose

         A3: x in ].( - ( sqrt 2)), ( - 1).[;

        then

         A4: ].( - ( sqrt 2)), ( - 1).[ c= [.( - ( sqrt 2)), ( - 1).] & ex s be Real st s = x & ( - ( sqrt 2)) < s & s < ( - 1) by XXREAL_1: 25;

        

         A5: ( [.( - ( sqrt 2)), ( - 1).] /\ ( dom arcsec2 )) = [.( - ( sqrt 2)), ( - 1).] by Th46, XBOOLE_1: 28;

        then ( - 1) in ( [.( - ( sqrt 2)), ( - 1).] /\ ( dom arcsec2 )) by A1;

        then

         A6: ( arcsec2 . x) < PI by A3, A5, A4, Th74, Th82, RFUNCT_2: 20;

        ( - ( sqrt 2)) in [.( - ( sqrt 2)), ( - 1).] by A1;

        then ((3 / 4) * PI ) < ( arcsec2 . x) by A3, A5, A4, Th74, Th82, RFUNCT_2: 20;

        hence thesis by A6;

      end;

        suppose

         A7: x = ( - ( sqrt 2));

        ((3 / 4) * PI ) <= PI by Lm6, XXREAL_1: 2;

        hence thesis by A7, Th74;

      end;

        suppose

         A8: x = ( - 1);

        ((3 / 4) * PI ) <= PI by Lm6, XXREAL_1: 2;

        hence thesis by A8, Th74;

      end;

    end;

    theorem :: SINCOS10:87

    

     Th87: for x be set st x in [.( - ( sqrt 2)), ( - 1).] holds ( arccosec1 . x) in [.( - ( PI / 2)), ( - ( PI / 4)).]

    proof

      let x be set;

      

       A1: ( - ( sqrt 2)) < ( - 1) by SQUARE_1: 19, XREAL_1: 24;

      assume x in [.( - ( sqrt 2)), ( - 1).];

      then x in ( ].( - ( sqrt 2)), ( - 1).[ \/ {( - ( sqrt 2)), ( - 1)}) by A1, XXREAL_1: 128;

      then

       A2: x in ].( - ( sqrt 2)), ( - 1).[ or x in {( - ( sqrt 2)), ( - 1)} by XBOOLE_0:def 3;

      per cases by A2, TARSKI:def 2;

        suppose

         A3: x in ].( - ( sqrt 2)), ( - 1).[;

        then

         A4: ].( - ( sqrt 2)), ( - 1).[ c= [.( - ( sqrt 2)), ( - 1).] & ex s be Real st s = x & ( - ( sqrt 2)) < s & s < ( - 1) by XXREAL_1: 25;

        

         A5: ( [.( - ( sqrt 2)), ( - 1).] /\ ( dom arccosec1 )) = [.( - ( sqrt 2)), ( - 1).] by Th47, XBOOLE_1: 28;

        then ( - 1) in ( [.( - ( sqrt 2)), ( - 1).] /\ ( dom arccosec1 )) by A1;

        then

         A6: ( arccosec1 . x) > ( - ( PI / 2)) by A3, A5, A4, Th75, Th83, RFUNCT_2: 21;

        ( - ( sqrt 2)) in [.( - ( sqrt 2)), ( - 1).] by A1;

        then ( - ( PI / 4)) > ( arccosec1 . x) by A3, A5, A4, Th75, Th83, RFUNCT_2: 21;

        hence thesis by A6;

      end;

        suppose

         A7: x = ( - ( sqrt 2));

        ( - ( PI / 2)) <= ( - ( PI / 4)) by Lm7, XXREAL_1: 3;

        hence thesis by A7, Th75;

      end;

        suppose

         A8: x = ( - 1);

        ( - ( PI / 2)) <= ( - ( PI / 4)) by Lm7, XXREAL_1: 3;

        hence thesis by A8, Th75;

      end;

    end;

    theorem :: SINCOS10:88

    

     Th88: for x be set st x in [.1, ( sqrt 2).] holds ( arccosec2 . x) in [.( PI / 4), ( PI / 2).]

    proof

      let x be set;

      assume x in [.1, ( sqrt 2).];

      then x in ( ].1, ( sqrt 2).[ \/ {1, ( sqrt 2)}) by SQUARE_1: 19, XXREAL_1: 128;

      then

       A1: x in ].1, ( sqrt 2).[ or x in {1, ( sqrt 2)} by XBOOLE_0:def 3;

      per cases by A1, TARSKI:def 2;

        suppose

         A2: x in ].1, ( sqrt 2).[;

        then

         A3: ].1, ( sqrt 2).[ c= [.1, ( sqrt 2).] & ex s be Real st s = x & 1 < s & s < ( sqrt 2) by XXREAL_1: 25;

        

         A4: ( [.1, ( sqrt 2).] /\ ( dom arccosec2 )) = [.1, ( sqrt 2).] by Th48, XBOOLE_1: 28;

        then ( sqrt 2) in ( [.1, ( sqrt 2).] /\ ( dom arccosec2 )) by SQUARE_1: 19;

        then

         A5: ( arccosec2 . x) > ( PI / 4) by A2, A4, A3, Th76, Th84, RFUNCT_2: 21;

        1 in [.1, ( sqrt 2).] by SQUARE_1: 19;

        then ( PI / 2) > ( arccosec2 . x) by A2, A4, A3, Th76, Th84, RFUNCT_2: 21;

        hence thesis by A5;

      end;

        suppose

         A6: x = 1;

        ( PI / 4) <= ( PI / 2) by Lm8, XXREAL_1: 2;

        hence thesis by A6, Th76;

      end;

        suppose

         A7: x = ( sqrt 2);

        ( PI / 4) <= ( PI / 2) by Lm8, XXREAL_1: 2;

        hence thesis by A7, Th76;

      end;

    end;

    theorem :: SINCOS10:89

    

     Th89: 1 <= r & r <= ( sqrt 2) implies ( sec . ( arcsec1 r)) = r

    proof

      assume 1 <= r & r <= ( sqrt 2);

      then

       A1: r in [.1, ( sqrt 2).];

      then

       A2: r in ( dom ( arcsec1 | [.1, ( sqrt 2).])) by Th45, RELAT_1: 62;

      ( sec . ( arcsec1 r)) = (( sec | [. 0 , ( PI / 4).]) qua Function . ( arcsec1 . r)) by A1, Th85, FUNCT_1: 49

      .= (( sec | [. 0 , ( PI / 4).]) qua Function . (( arcsec1 | [.1, ( sqrt 2).]) . r)) by A1, FUNCT_1: 49

      .= ((( sec | [. 0 , ( PI / 4).]) qua Function * ( arcsec1 | [.1, ( sqrt 2).])) . r) by A2, FUNCT_1: 13

      .= (( id [.1, ( sqrt 2).]) . r) by Th41, Th49, FUNCT_1: 39

      .= r by A1, FUNCT_1: 18;

      hence thesis;

    end;

    theorem :: SINCOS10:90

    

     Th90: ( - ( sqrt 2)) <= r & r <= ( - 1) implies ( sec . ( arcsec2 r)) = r

    proof

      assume ( - ( sqrt 2)) <= r & r <= ( - 1);

      then

       A1: r in [.( - ( sqrt 2)), ( - 1).];

      then

       A2: r in ( dom ( arcsec2 | [.( - ( sqrt 2)), ( - 1).])) by Th46, RELAT_1: 62;

      ( sec . ( arcsec2 r)) = (( sec | [.((3 / 4) * PI ), PI .]) qua Function . ( arcsec2 . r)) by A1, Th86, FUNCT_1: 49

      .= (( sec | [.((3 / 4) * PI ), PI .]) qua Function . (( arcsec2 | [.( - ( sqrt 2)), ( - 1).]) . r)) by A1, FUNCT_1: 49

      .= ((( sec | [.((3 / 4) * PI ), PI .]) qua Function * ( arcsec2 | [.( - ( sqrt 2)), ( - 1).])) . r) by A2, FUNCT_1: 13

      .= (( id [.( - ( sqrt 2)), ( - 1).]) . r) by Th42, Th50, FUNCT_1: 39

      .= r by A1, FUNCT_1: 18;

      hence thesis;

    end;

    theorem :: SINCOS10:91

    

     Th91: ( - ( sqrt 2)) <= r & r <= ( - 1) implies ( cosec . ( arccosec1 r)) = r

    proof

      assume ( - ( sqrt 2)) <= r & r <= ( - 1);

      then

       A1: r in [.( - ( sqrt 2)), ( - 1).];

      then

       A2: r in ( dom ( arccosec1 | [.( - ( sqrt 2)), ( - 1).])) by Th47, RELAT_1: 62;

      ( cosec . ( arccosec1 r)) = (( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) qua Function . ( arccosec1 . r)) by A1, Th87, FUNCT_1: 49

      .= (( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) qua Function . (( arccosec1 | [.( - ( sqrt 2)), ( - 1).]) . r)) by A1, FUNCT_1: 49

      .= ((( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]) qua Function * ( arccosec1 | [.( - ( sqrt 2)), ( - 1).])) . r) by A2, FUNCT_1: 13

      .= (( id [.( - ( sqrt 2)), ( - 1).]) . r) by Th43, Th51, FUNCT_1: 39

      .= r by A1, FUNCT_1: 18;

      hence thesis;

    end;

    theorem :: SINCOS10:92

    

     Th92: 1 <= r & r <= ( sqrt 2) implies ( cosec . ( arccosec2 r)) = r

    proof

      assume 1 <= r & r <= ( sqrt 2);

      then

       A1: r in [.1, ( sqrt 2).];

      then

       A2: r in ( dom ( arccosec2 | [.1, ( sqrt 2).])) by Th48, RELAT_1: 62;

      ( cosec . ( arccosec2 r)) = (( cosec | [.( PI / 4), ( PI / 2).]) qua Function . ( arccosec2 . r)) by A1, Th88, FUNCT_1: 49

      .= (( cosec | [.( PI / 4), ( PI / 2).]) qua Function . (( arccosec2 | [.1, ( sqrt 2).]) . r)) by A1, FUNCT_1: 49

      .= ((( cosec | [.( PI / 4), ( PI / 2).]) qua Function * ( arccosec2 | [.1, ( sqrt 2).])) . r) by A2, FUNCT_1: 13

      .= (( id [.1, ( sqrt 2).]) . r) by Th44, Th52, FUNCT_1: 39

      .= r by A1, FUNCT_1: 18;

      hence thesis;

    end;

    theorem :: SINCOS10:93

    

     Th93: ( arcsec1 | [.1, ( sqrt 2).]) is continuous

    proof

      set f = ( sec | [. 0 , ( PI / 4).]);

      (f | [. 0 , ( PI / 4).]) = f & (((f | [. 0 , ( PI / 4).]) " ) | (f .: [. 0 , ( PI / 4).])) is continuous by Lm29, Lm37, FCONT_1: 47, RELAT_1: 72;

      then (( arcsec1 | [.1, ( sqrt 2).]) | [.1, ( sqrt 2).]) is continuous by Th41, Th49, RELAT_1: 115;

      hence thesis by FCONT_1: 15;

    end;

    theorem :: SINCOS10:94

    

     Th94: ( arcsec2 | [.( - ( sqrt 2)), ( - 1).]) is continuous

    proof

      set f = ( sec | [.((3 / 4) * PI ), PI .]);

      ((3 / 4) * PI ) <= PI by Lm6, XXREAL_1: 2;

      then (f | [.((3 / 4) * PI ), PI .]) = f & (((f | [.((3 / 4) * PI ), PI .]) " ) | (f .: [.((3 / 4) * PI ), PI .])) is continuous by Lm30, Lm38, FCONT_1: 47, RELAT_1: 72;

      then (( arcsec2 | [.( - ( sqrt 2)), ( - 1).]) | [.( - ( sqrt 2)), ( - 1).]) is continuous by Th42, Th50, RELAT_1: 115;

      hence thesis by FCONT_1: 15;

    end;

    theorem :: SINCOS10:95

    

     Th95: ( arccosec1 | [.( - ( sqrt 2)), ( - 1).]) is continuous

    proof

      set f = ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).]);

      ( - ( PI / 2)) <= ( - ( PI / 4)) by Lm7, XXREAL_1: 3;

      then (f | [.( - ( PI / 2)), ( - ( PI / 4)).]) = f & (((f | [.( - ( PI / 2)), ( - ( PI / 4)).]) " ) | (f .: [.( - ( PI / 2)), ( - ( PI / 4)).])) is continuous by Lm31, Lm39, FCONT_1: 47, RELAT_1: 72;

      then (( arccosec1 | [.( - ( sqrt 2)), ( - 1).]) | [.( - ( sqrt 2)), ( - 1).]) is continuous by Th43, Th51, RELAT_1: 115;

      hence thesis by FCONT_1: 15;

    end;

    theorem :: SINCOS10:96

    

     Th96: ( arccosec2 | [.1, ( sqrt 2).]) is continuous

    proof

      set f = ( cosec | [.( PI / 4), ( PI / 2).]);

      ( PI / 4) <= ( PI / 2) by Lm8, XXREAL_1: 2;

      then (f | [.( PI / 4), ( PI / 2).]) = f & (((f | [.( PI / 4), ( PI / 2).]) " ) | (f .: [.( PI / 4), ( PI / 2).])) is continuous by Lm32, Lm40, FCONT_1: 47, RELAT_1: 72;

      then (( arccosec2 | [.1, ( sqrt 2).]) | [.1, ( sqrt 2).]) is continuous by Th44, Th52, RELAT_1: 115;

      hence thesis by FCONT_1: 15;

    end;

    theorem :: SINCOS10:97

    

     Th97: ( rng ( arcsec1 | [.1, ( sqrt 2).])) = [. 0 , ( PI / 4).]

    proof

      now

        let y be object;

        thus y in [. 0 , ( PI / 4).] implies ex x be object st x in ( dom ( arcsec1 | [.1, ( sqrt 2).])) & y = (( arcsec1 | [.1, ( sqrt 2).]) . x)

        proof

          assume

           A1: y in [. 0 , ( PI / 4).];

          then

          reconsider y1 = y as Real;

          y1 in ( [.( arcsec1 . 1), ( arcsec1 . ( sqrt 2)).] \/ [.( arcsec1 . ( sqrt 2)), ( arcsec1 . 1).]) by A1, Th73, XBOOLE_0:def 3;

          then

          consider x be Real such that

           A2: x in [.1, ( sqrt 2).] & y1 = ( arcsec1 . x) by Th45, Th93, FCONT_2: 15, SQUARE_1: 19;

          take x;

          thus thesis by A2, Th45, FUNCT_1: 49, RELAT_1: 62;

        end;

        thus (ex x be object st x in ( dom ( arcsec1 | [.1, ( sqrt 2).])) & y = (( arcsec1 | [.1, ( sqrt 2).]) . x)) implies y in [. 0 , ( PI / 4).]

        proof

          given x be object such that

           A3: x in ( dom ( arcsec1 | [.1, ( sqrt 2).])) and

           A4: y = (( arcsec1 | [.1, ( sqrt 2).]) . x);

          

           A5: ( dom ( arcsec1 | [.1, ( sqrt 2).])) = [.1, ( sqrt 2).] by Th45, RELAT_1: 62;

          then y = ( arcsec1 . x) by A3, A4, FUNCT_1: 49;

          hence thesis by A3, A5, Th85;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: SINCOS10:98

    

     Th98: ( rng ( arcsec2 | [.( - ( sqrt 2)), ( - 1).])) = [.((3 / 4) * PI ), PI .]

    proof

      now

        let y be object;

        thus y in [.((3 / 4) * PI ), PI .] implies ex x be object st x in ( dom ( arcsec2 | [.( - ( sqrt 2)), ( - 1).])) & y = (( arcsec2 | [.( - ( sqrt 2)), ( - 1).]) . x)

        proof

          assume

           A1: y in [.((3 / 4) * PI ), PI .];

          then

          reconsider y1 = y as Real;

          ( - ( sqrt 2)) < ( - 1) & y1 in ( [.( arcsec2 . ( - ( sqrt 2))), ( arcsec2 . ( - 1)).] \/ [.( arcsec2 . ( - 1)), ( arcsec2 . ( - ( sqrt 2))).]) by A1, Th74, SQUARE_1: 19, XBOOLE_0:def 3, XREAL_1: 24;

          then

          consider x be Real such that

           A2: x in [.( - ( sqrt 2)), ( - 1).] & y1 = ( arcsec2 . x) by Th46, Th94, FCONT_2: 15;

          take x;

          thus thesis by A2, Th46, FUNCT_1: 49, RELAT_1: 62;

        end;

        thus (ex x be object 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 object such that

           A3: x in ( dom ( arcsec2 | [.( - ( sqrt 2)), ( - 1).])) and

           A4: y = (( arcsec2 | [.( - ( sqrt 2)), ( - 1).]) . x);

          

           A5: ( dom ( arcsec2 | [.( - ( sqrt 2)), ( - 1).])) = [.( - ( sqrt 2)), ( - 1).] by Th46, RELAT_1: 62;

          then y = ( arcsec2 . x) by A3, A4, FUNCT_1: 49;

          hence thesis by A3, A5, Th86;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: SINCOS10:99

    

     Th99: ( rng ( arccosec1 | [.( - ( sqrt 2)), ( - 1).])) = [.( - ( PI / 2)), ( - ( PI / 4)).]

    proof

      now

        let y be object;

        thus y in [.( - ( PI / 2)), ( - ( PI / 4)).] implies ex x be object st x in ( dom ( arccosec1 | [.( - ( sqrt 2)), ( - 1).])) & y = (( arccosec1 | [.( - ( sqrt 2)), ( - 1).]) . x)

        proof

          assume

           A1: y in [.( - ( PI / 2)), ( - ( PI / 4)).];

          then

          reconsider y1 = y as Real;

          ( - ( sqrt 2)) < ( - 1) & y1 in ( [.( arccosec1 . ( - 1)), ( arccosec1 . ( - ( sqrt 2))).] \/ [.( arccosec1 . ( - ( sqrt 2))), ( arccosec1 . ( - 1)).]) by A1, Th75, SQUARE_1: 19, XBOOLE_0:def 3, XREAL_1: 24;

          then

          consider x be Real such that

           A2: x in [.( - ( sqrt 2)), ( - 1).] & y1 = ( arccosec1 . x) by Th47, Th95, FCONT_2: 15;

          take x;

          thus thesis by A2, Th47, FUNCT_1: 49, RELAT_1: 62;

        end;

        thus (ex x be object 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 object such that

           A3: x in ( dom ( arccosec1 | [.( - ( sqrt 2)), ( - 1).])) and

           A4: y = (( arccosec1 | [.( - ( sqrt 2)), ( - 1).]) . x);

          

           A5: ( dom ( arccosec1 | [.( - ( sqrt 2)), ( - 1).])) = [.( - ( sqrt 2)), ( - 1).] by Th47, RELAT_1: 62;

          then y = ( arccosec1 . x) by A3, A4, FUNCT_1: 49;

          hence thesis by A3, A5, Th87;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: SINCOS10:100

    

     Th100: ( rng ( arccosec2 | [.1, ( sqrt 2).])) = [.( PI / 4), ( PI / 2).]

    proof

      now

        let y be object;

        thus y in [.( PI / 4), ( PI / 2).] implies ex x be object st x in ( dom ( arccosec2 | [.1, ( sqrt 2).])) & y = (( arccosec2 | [.1, ( sqrt 2).]) . x)

        proof

          assume

           A1: y in [.( PI / 4), ( PI / 2).];

          then

          reconsider y1 = y as Real;

          y1 in ( [.( arccosec2 . ( sqrt 2)), ( arccosec2 . 1).] \/ [.( arccosec2 . 1), ( arccosec2 . ( sqrt 2)).]) by A1, Th76, XBOOLE_0:def 3;

          then

          consider x be Real such that

           A2: x in [.1, ( sqrt 2).] & y1 = ( arccosec2 . x) by Th48, Th96, FCONT_2: 15, SQUARE_1: 19;

          take x;

          thus thesis by A2, Th48, FUNCT_1: 49, RELAT_1: 62;

        end;

        thus (ex x be object 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 object such that

           A3: x in ( dom ( arccosec2 | [.1, ( sqrt 2).])) and

           A4: y = (( arccosec2 | [.1, ( sqrt 2).]) . x);

          

           A5: ( dom ( arccosec2 | [.1, ( sqrt 2).])) = [.1, ( sqrt 2).] by Th48, RELAT_1: 62;

          then y = ( arccosec2 . x) by A3, A4, FUNCT_1: 49;

          hence thesis by A3, A5, Th88;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: SINCOS10:101

    (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 :: SINCOS10:102

    (( - ( 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 :: SINCOS10:103

    (( - ( 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 :: SINCOS10:104

    (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 :: SINCOS10:105

    

     Th105: 1 <= r & r <= ( sqrt 2) implies 0 <= ( arcsec1 r) & ( arcsec1 r) <= ( PI / 4)

    proof

      assume 1 <= r & r <= ( sqrt 2);

      then

       A1: r in [.1, ( sqrt 2).];

      then r in ( dom ( arcsec1 | [.1, ( sqrt 2).])) by Th45, RELAT_1: 62;

      then (( arcsec1 | [.1, ( sqrt 2).]) . r) in ( rng ( arcsec1 | [.1, ( sqrt 2).])) by FUNCT_1:def 3;

      then ( arcsec1 r) in ( rng ( arcsec1 | [.1, ( sqrt 2).])) by A1, FUNCT_1: 49;

      hence thesis by Th97, XXREAL_1: 1;

    end;

    theorem :: SINCOS10:106

    

     Th106: ( - ( sqrt 2)) <= r & r <= ( - 1) implies ((3 / 4) * PI ) <= ( arcsec2 r) & ( arcsec2 r) <= PI

    proof

      assume ( - ( sqrt 2)) <= r & r <= ( - 1);

      then

       A1: r in [.( - ( sqrt 2)), ( - 1).];

      then r in ( dom ( arcsec2 | [.( - ( sqrt 2)), ( - 1).])) by Th46, RELAT_1: 62;

      then (( arcsec2 | [.( - ( sqrt 2)), ( - 1).]) . r) in ( rng ( arcsec2 | [.( - ( sqrt 2)), ( - 1).])) by FUNCT_1:def 3;

      then ( arcsec2 r) in ( rng ( arcsec2 | [.( - ( sqrt 2)), ( - 1).])) by A1, FUNCT_1: 49;

      hence thesis by Th98, XXREAL_1: 1;

    end;

    theorem :: SINCOS10:107

    

     Th107: ( - ( sqrt 2)) <= r & r <= ( - 1) implies ( - ( PI / 2)) <= ( arccosec1 r) & ( arccosec1 r) <= ( - ( PI / 4))

    proof

      assume ( - ( sqrt 2)) <= r & r <= ( - 1);

      then

       A1: r in [.( - ( sqrt 2)), ( - 1).];

      then r in ( dom ( arccosec1 | [.( - ( sqrt 2)), ( - 1).])) by Th47, RELAT_1: 62;

      then (( arccosec1 | [.( - ( sqrt 2)), ( - 1).]) . r) in ( rng ( arccosec1 | [.( - ( sqrt 2)), ( - 1).])) by FUNCT_1:def 3;

      then ( arccosec1 r) in ( rng ( arccosec1 | [.( - ( sqrt 2)), ( - 1).])) by A1, FUNCT_1: 49;

      hence thesis by Th99, XXREAL_1: 1;

    end;

    theorem :: SINCOS10:108

    

     Th108: 1 <= r & r <= ( sqrt 2) implies ( PI / 4) <= ( arccosec2 r) & ( arccosec2 r) <= ( PI / 2)

    proof

      assume 1 <= r & r <= ( sqrt 2);

      then

       A1: r in [.1, ( sqrt 2).];

      then r in ( dom ( arccosec2 | [.1, ( sqrt 2).])) by Th48, RELAT_1: 62;

      then (( arccosec2 | [.1, ( sqrt 2).]) . r) in ( rng ( arccosec2 | [.1, ( sqrt 2).])) by FUNCT_1:def 3;

      then ( arccosec2 r) in ( rng ( arccosec2 | [.1, ( sqrt 2).])) by A1, FUNCT_1: 49;

      hence thesis by Th100, XXREAL_1: 1;

    end;

    theorem :: SINCOS10:109

    

     Th109: 1 < r & r < ( sqrt 2) implies 0 < ( arcsec1 r) & ( arcsec1 r) < ( PI / 4)

    proof

      assume

       A1: 1 < r & r < ( sqrt 2);

      then ( arcsec1 r) <= ( PI / 4) by Th105;

      then 0 < ( arcsec1 r) & ( arcsec1 r) < ( PI / 4) or 0 = ( arcsec1 r) or ( arcsec1 r) = ( PI / 4) by A1, Th105, XXREAL_0: 1;

      hence thesis by A1, Th31, Th89;

    end;

    theorem :: SINCOS10:110

    

     Th110: ( - ( sqrt 2)) < r & r < ( - 1) implies ((3 / 4) * PI ) < ( arcsec2 r) & ( arcsec2 r) < PI

    proof

      assume

       A1: ( - ( sqrt 2)) < r & r < ( - 1);

      then ((3 / 4) * PI ) <= ( arcsec2 r) & ( arcsec2 r) <= PI by Th106;

      then ((3 / 4) * PI ) < ( arcsec2 r) & ( arcsec2 r) < PI or ((3 / 4) * PI ) = ( arcsec2 r) or ( arcsec2 r) = PI by XXREAL_0: 1;

      hence thesis by A1, Th31, Th90;

    end;

    theorem :: SINCOS10:111

    

     Th111: ( - ( sqrt 2)) < r & r < ( - 1) implies ( - ( PI / 2)) < ( arccosec1 r) & ( arccosec1 r) < ( - ( PI / 4))

    proof

      assume

       A1: ( - ( sqrt 2)) < r & r < ( - 1);

      then ( - ( PI / 2)) <= ( arccosec1 r) & ( arccosec1 r) <= ( - ( PI / 4)) by Th107;

      then ( - ( PI / 2)) < ( arccosec1 r) & ( arccosec1 r) < ( - ( PI / 4)) or ( - ( PI / 2)) = ( arccosec1 r) or ( arccosec1 r) = ( - ( PI / 4)) by XXREAL_0: 1;

      hence thesis by A1, Th32, Th91;

    end;

    theorem :: SINCOS10:112

    

     Th112: 1 < r & r < ( sqrt 2) implies ( PI / 4) < ( arccosec2 r) & ( arccosec2 r) < ( PI / 2)

    proof

      assume

       A1: 1 < r & r < ( sqrt 2);

      then ( PI / 4) <= ( arccosec2 r) & ( arccosec2 r) <= ( PI / 2) by Th108;

      then ( PI / 4) < ( arccosec2 r) & ( arccosec2 r) < ( PI / 2) or ( PI / 4) = ( arccosec2 r) or ( arccosec2 r) = ( PI / 2) by XXREAL_0: 1;

      hence thesis by A1, Th32, Th92;

    end;

    theorem :: SINCOS10:113

    

     Th113: 1 <= r & r <= ( sqrt 2) implies ( sin . ( arcsec1 r)) = (( sqrt ((r ^2 ) - 1)) / r) & ( cos . ( arcsec1 r)) = (1 / r)

    proof

      set x = ( arcsec1 r);

      assume that

       A1: 1 <= r and

       A2: r <= ( sqrt 2);

      r in [.1, ( sqrt 2).] by A1, A2;

      then

       A3: x in ( dom ( sec | [. 0 , ( PI / 4).])) by Lm29, Th85;

      ( PI / 4) < ( PI / 1) by XREAL_1: 76;

      then 0 in [. 0 , PI .] & ( PI / 4) in [. 0 , PI .];

      then [. 0 , ( PI / 4).] c= [. 0 , PI .] by XXREAL_2:def 12;

      then

       A4: ( sin . x) >= 0 by A3, Lm29, COMPTRIG: 8;

      

       A5: ( dom ( sec | [. 0 , ( PI / 4).])) c= ( dom sec ) by RELAT_1: 60;

      

       A6: r = (( cos ^ ) . x) by A1, A2, Th89

      .= (1 / ( cos . x)) by A3, A5, RFUNCT_1:def 2;

      (r ^2 ) >= (1 ^2 ) by A1, SQUARE_1: 15;

      then

       A7: ((r ^2 ) - 1) >= 0 by XREAL_1: 48;

      ((( sin . x) ^2 ) + (( cos . x) ^2 )) = 1 by SIN_COS: 28;

      

      then (( sin . x) ^2 ) = (1 - (( cos . x) ^2 ))

      .= (1 - ((1 / r) * (1 / r))) by A6

      .= (1 - (1 / (r ^2 ))) by XCMPLX_1: 102

      .= (((r ^2 ) / (r ^2 )) - (1 / (r ^2 ))) by A1, XCMPLX_1: 60

      .= (((r ^2 ) - 1) / (r ^2 ));

      

      then ( sin . x) = ( sqrt (((r ^2 ) - 1) / (r ^2 ))) by A4, SQUARE_1:def 2

      .= (( sqrt ((r ^2 ) - 1)) / ( sqrt (r ^2 ))) by A1, A7, SQUARE_1: 30

      .= (( sqrt ((r ^2 ) - 1)) / r) by A1, SQUARE_1: 22;

      hence thesis by A6;

    end;

    theorem :: SINCOS10:114

    

     Th114: ( - ( sqrt 2)) <= r & r <= ( - 1) implies ( sin . ( arcsec2 r)) = ( - (( sqrt ((r ^2 ) - 1)) / r)) & ( cos . ( arcsec2 r)) = (1 / r)

    proof

      ((3 / 4) * PI ) <= PI by Lm6, XXREAL_1: 2;

      then

       A1: ((3 / 4) * PI ) in [. 0 , PI .];

      

       A2: ( dom ( sec | [.((3 / 4) * PI ), PI .])) c= ( dom sec ) by RELAT_1: 60;

      set x = ( arcsec2 r);

      assume that

       A3: ( - ( sqrt 2)) <= r and

       A4: r <= ( - 1);

      r in [.( - ( sqrt 2)), ( - 1).] by A3, A4;

      then

       A5: x in ( dom ( sec | [.((3 / 4) * PI ), PI .])) by Lm30, Th86;

      

       A6: r = (( cos ^ ) . x) by A3, A4, Th90

      .= (1 / ( cos . x)) by A5, A2, RFUNCT_1:def 2;

       PI in [. 0 , PI .];

      then [.((3 / 4) * PI ), PI .] c= [. 0 , PI .] by A1, XXREAL_2:def 12;

      then

       A7: ( sin . x) >= 0 by A5, Lm30, COMPTRIG: 8;

      ( - r) >= ( - ( - 1)) by A4, XREAL_1: 24;

      then (( - r) ^2 ) >= (1 ^2 ) by SQUARE_1: 15;

      then

       A8: ((r ^2 ) - 1) >= 0 by XREAL_1: 48;

      ((( sin . x) ^2 ) + (( cos . x) ^2 )) = 1 by SIN_COS: 28;

      

      then (( sin . x) ^2 ) = (1 - (( cos . x) ^2 ))

      .= (1 - ((1 / r) * (1 / r))) by A6

      .= (1 - (1 / (r ^2 ))) by XCMPLX_1: 102

      .= (((r ^2 ) / (r ^2 )) - (1 / (r ^2 ))) by A4, XCMPLX_1: 60

      .= (((r ^2 ) - 1) / (r ^2 ));

      

      then ( sin . x) = ( sqrt (((r ^2 ) - 1) / (r ^2 ))) by A7, SQUARE_1:def 2

      .= (( sqrt ((r ^2 ) - 1)) / ( sqrt (r ^2 ))) by A4, A8, SQUARE_1: 30

      .= (( sqrt ((r ^2 ) - 1)) / ( - r)) by A4, SQUARE_1: 23

      .= ( - (( sqrt ((r ^2 ) - 1)) / r)) by XCMPLX_1: 188;

      hence thesis by A6;

    end;

    theorem :: SINCOS10:115

    

     Th115: ( - ( sqrt 2)) <= r & r <= ( - 1) implies ( sin . ( arccosec1 r)) = (1 / r) & ( cos . ( arccosec1 r)) = ( - (( sqrt ((r ^2 ) - 1)) / r))

    proof

      set x = ( arccosec1 r);

      assume that

       A1: ( - ( sqrt 2)) <= r and

       A2: r <= ( - 1);

      r in [.( - ( sqrt 2)), ( - 1).] by A1, A2;

      then

       A3: x in ( dom ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).])) by Lm31, Th87;

      ( - ( PI / 4)) >= ( - ( PI / 2)) by Lm7, XXREAL_1: 3;

      then ( - ( PI / 2)) in [.( - ( PI / 2)), ( PI / 2).] & ( - ( PI / 4)) in [.( - ( PI / 2)), ( PI / 2).];

      then [.( - ( PI / 2)), ( - ( PI / 4)).] c= [.( - ( PI / 2)), ( PI / 2).] by XXREAL_2:def 12;

      then

       A4: ( cos . x) >= 0 by A3, Lm31, COMPTRIG: 12;

      

       A5: ( dom ( cosec | [.( - ( PI / 2)), ( - ( PI / 4)).])) c= ( dom cosec ) by RELAT_1: 60;

      

       A6: r = (( sin ^ ) . x) by A1, A2, Th91

      .= (1 / ( sin . x)) by A3, A5, RFUNCT_1:def 2;

      ( - r) >= ( - ( - 1)) by A2, XREAL_1: 24;

      then (( - r) ^2 ) >= (1 ^2 ) by SQUARE_1: 15;

      then

       A7: ((r ^2 ) - 1) >= 0 by XREAL_1: 48;

      ((( sin . x) ^2 ) + (( cos . x) ^2 )) = 1 by SIN_COS: 28;

      

      then (( cos . x) ^2 ) = (1 - (( sin . x) ^2 ))

      .= (1 - ((1 / r) * (1 / r))) by A6

      .= (1 - (1 / (r ^2 ))) by XCMPLX_1: 102

      .= (((r ^2 ) / (r ^2 )) - (1 / (r ^2 ))) by A2, XCMPLX_1: 60

      .= (((r ^2 ) - 1) / (r ^2 ));

      

      then ( cos . x) = ( sqrt (((r ^2 ) - 1) / (r ^2 ))) by A4, SQUARE_1:def 2

      .= (( sqrt ((r ^2 ) - 1)) / ( sqrt (r ^2 ))) by A2, A7, SQUARE_1: 30

      .= (( sqrt ((r ^2 ) - 1)) / ( - r)) by A2, SQUARE_1: 23

      .= ( - (( sqrt ((r ^2 ) - 1)) / r)) by XCMPLX_1: 188;

      hence thesis by A6;

    end;

    theorem :: SINCOS10:116

    

     Th116: 1 <= r & r <= ( sqrt 2) implies ( sin . ( arccosec2 r)) = (1 / r) & ( cos . ( arccosec2 r)) = (( sqrt ((r ^2 ) - 1)) / r)

    proof

      ( PI / 4) <= ( PI / 2) by Lm8, XXREAL_1: 2;

      then

       A1: ( PI / 4) in [.( - ( PI / 2)), ( PI / 2).];

      

       A2: ( dom ( cosec | [.( PI / 4), ( PI / 2).])) c= ( dom cosec ) by RELAT_1: 60;

      set x = ( arccosec2 r);

      assume that

       A3: 1 <= r and

       A4: r <= ( sqrt 2);

      r in [.1, ( sqrt 2).] by A3, A4;

      then

       A5: x in ( dom ( cosec | [.( PI / 4), ( PI / 2).])) by Lm32, Th88;

      

       A6: r = (( sin ^ ) . x) by A3, A4, Th92

      .= (1 / ( sin . x)) by A5, A2, RFUNCT_1:def 2;

      ( PI / 2) in [.( - ( PI / 2)), ( PI / 2).];

      then [.( PI / 4), ( PI / 2).] c= [.( - ( PI / 2)), ( PI / 2).] by A1, XXREAL_2:def 12;

      then

       A7: ( cos . x) >= 0 by A5, Lm32, COMPTRIG: 12;

      (r ^2 ) >= (1 ^2 ) by A3, SQUARE_1: 15;

      then

       A8: ((r ^2 ) - 1) >= 0 by XREAL_1: 48;

      ((( sin . x) ^2 ) + (( cos . x) ^2 )) = 1 by SIN_COS: 28;

      

      then (( cos . x) ^2 ) = (1 - (( sin . x) ^2 ))

      .= (1 - ((1 / r) * (1 / r))) by A6

      .= (1 - (1 / (r ^2 ))) by XCMPLX_1: 102

      .= (((r ^2 ) / (r ^2 )) - (1 / (r ^2 ))) by A3, XCMPLX_1: 60

      .= (((r ^2 ) - 1) / (r ^2 ));

      

      then ( cos . x) = ( sqrt (((r ^2 ) - 1) / (r ^2 ))) by A7, SQUARE_1:def 2

      .= (( sqrt ((r ^2 ) - 1)) / ( sqrt (r ^2 ))) by A3, A8, SQUARE_1: 30

      .= (( sqrt ((r ^2 ) - 1)) / r) by A3, SQUARE_1: 22;

      hence thesis by A6;

    end;

    theorem :: SINCOS10:117

    1 < r & r < ( sqrt 2) implies ( cosec . ( arcsec1 r)) = (r / ( sqrt ((r ^2 ) - 1)))

    proof

      set x = ( arcsec1 r);

       ]. 0 , ( PI / 2).] = ( ]. 0 , ( PI / 2).[ \/ {( PI / 2)}) by XXREAL_1: 132;

      then

       A1: ]. 0 , ( PI / 2).[ c= ]. 0 , ( PI / 2).] by XBOOLE_1: 7;

      ( PI / 4) < ( PI / 2) by XREAL_1: 76;

      then ]. 0 , ( PI / 4).[ c= ]. 0 , ( PI / 2).[ by XXREAL_1: 46;

      then ]. 0 , ( PI / 4).[ c= ]. 0 , ( PI / 2).] by A1;

      then

       A2: ]. 0 , ( PI / 4).[ c= ( dom cosec ) by Th4;

      assume

       A3: 1 < r & r < ( sqrt 2);

      then 0 < ( arcsec1 r) & ( arcsec1 r) < ( PI / 4) by Th109;

      then x in ]. 0 , ( PI / 4).[;

      

      then ( cosec . x) = (1 / ( sin . x)) by A2, RFUNCT_1:def 2

      .= (1 / (( sqrt ((r ^2 ) - 1)) / r)) by A3, Th113

      .= (r / ( sqrt ((r ^2 ) - 1))) by XCMPLX_1: 57;

      hence thesis;

    end;

    theorem :: SINCOS10:118

    ( - ( sqrt 2)) < r & r < ( - 1) implies ( cosec . ( arcsec2 r)) = ( - (r / ( sqrt ((r ^2 ) - 1))))

    proof

      set x = ( arcsec2 r);

      

       A1: ].((3 / 4) * PI ), PI .[ c= ( dom cosec )

      proof

        ( ].((3 / 4) * PI ), PI .[ /\ ( sin " { 0 })) = {}

        proof

          assume ( ].((3 / 4) * PI ), PI .[ /\ ( sin " { 0 })) <> {} ;

          then

          consider rr be object such that

           A2: rr in ( ].((3 / 4) * PI ), PI .[ /\ ( sin " { 0 })) by XBOOLE_0:def 1;

          rr in ( sin " { 0 }) by A2, XBOOLE_0:def 4;

          then

           A3: ( sin . rr) in { 0 } by FUNCT_1:def 7;

          

           A4: ].((3 / 4) * PI ), PI .[ c= ]. 0 , PI .[ by XXREAL_1: 46;

          rr in ].((3 / 4) * PI ), PI .[ by A2, XBOOLE_0:def 4;

          then ( sin . rr) <> 0 by A4, COMPTRIG: 7;

          hence contradiction by A3, TARSKI:def 1;

        end;

        then ( ].((3 / 4) * PI ), PI .[ \ ( sin " { 0 })) c= (( dom sin ) \ ( sin " { 0 })) & ].((3 / 4) * PI ), PI .[ misses ( sin " { 0 }) by SIN_COS: 24, XBOOLE_0:def 7, XBOOLE_1: 33;

        then ].((3 / 4) * PI ), PI .[ c= (( dom sin ) \ ( sin " { 0 })) by XBOOLE_1: 83;

        hence thesis by RFUNCT_1:def 2;

      end;

      assume

       A5: ( - ( sqrt 2)) < r & r < ( - 1);

      then ((3 / 4) * PI ) < ( arcsec2 r) & ( arcsec2 r) < PI by Th110;

      then x in ].((3 / 4) * PI ), PI .[;

      

      then ( cosec . x) = (1 / ( sin . x)) by A1, RFUNCT_1:def 2

      .= (1 / ( - (( sqrt ((r ^2 ) - 1)) / r))) by A5, Th114

      .= ( - (1 / (( sqrt ((r ^2 ) - 1)) / r))) by XCMPLX_1: 188

      .= ( - (r / ( sqrt ((r ^2 ) - 1)))) by XCMPLX_1: 57;

      hence thesis;

    end;

    theorem :: SINCOS10:119

    ( - ( sqrt 2)) < r & r < ( - 1) implies ( sec . ( arccosec1 r)) = ( - (r / ( sqrt ((r ^2 ) - 1))))

    proof

      set x = ( arccosec1 r);

      

       A1: ].( - ( PI / 2)), ( - ( PI / 4)).[ c= ( dom sec )

      proof

        ( ].( - ( PI / 2)), ( - ( PI / 4)).[ /\ ( cos " { 0 })) = {}

        proof

          assume ( ].( - ( PI / 2)), ( - ( PI / 4)).[ /\ ( cos " { 0 })) <> {} ;

          then

          consider rr be object such that

           A2: rr in ( ].( - ( PI / 2)), ( - ( PI / 4)).[ /\ ( cos " { 0 })) by XBOOLE_0:def 1;

          rr in ( cos " { 0 }) by A2, XBOOLE_0:def 4;

          then

           A3: ( cos . rr) in { 0 } by FUNCT_1:def 7;

          

           A4: ].( - ( PI / 2)), ( - ( PI / 4)).[ c= ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 46;

          rr in ].( - ( PI / 2)), ( - ( PI / 4)).[ by A2, XBOOLE_0:def 4;

          then ( cos . rr) <> 0 by A4, COMPTRIG: 11;

          hence contradiction by A3, TARSKI:def 1;

        end;

        then ( ].( - ( PI / 2)), ( - ( PI / 4)).[ \ ( cos " { 0 })) c= (( dom cos ) \ ( cos " { 0 })) & ].( - ( PI / 2)), ( - ( PI / 4)).[ misses ( cos " { 0 }) by SIN_COS: 24, XBOOLE_0:def 7, XBOOLE_1: 33;

        then ].( - ( PI / 2)), ( - ( PI / 4)).[ c= (( dom cos ) \ ( cos " { 0 })) by XBOOLE_1: 83;

        hence thesis by RFUNCT_1:def 2;

      end;

      assume

       A5: ( - ( sqrt 2)) < r & r < ( - 1);

      then ( - ( PI / 2)) < ( arccosec1 r) & ( arccosec1 r) < ( - ( PI / 4)) by Th111;

      then x in ].( - ( PI / 2)), ( - ( PI / 4)).[;

      

      then ( sec . x) = (1 / ( cos . x)) by A1, RFUNCT_1:def 2

      .= (1 / ( - (( sqrt ((r ^2 ) - 1)) / r))) by A5, Th115

      .= ( - (1 / (( sqrt ((r ^2 ) - 1)) / r))) by XCMPLX_1: 188

      .= ( - (r / ( sqrt ((r ^2 ) - 1)))) by XCMPLX_1: 57;

      hence thesis;

    end;

    theorem :: SINCOS10:120

    1 < r & r < ( sqrt 2) implies ( sec . ( arccosec2 r)) = (r / ( sqrt ((r ^2 ) - 1)))

    proof

      set x = ( arccosec2 r);

       [. 0 , ( PI / 2).[ = ( ]. 0 , ( PI / 2).[ \/ { 0 }) by XXREAL_1: 131;

      then ].( PI / 4), ( PI / 2).[ c= ]. 0 , ( PI / 2).[ & ]. 0 , ( PI / 2).[ c= [. 0 , ( PI / 2).[ by XBOOLE_1: 7, XXREAL_1: 46;

      then ].( PI / 4), ( PI / 2).[ c= [. 0 , ( PI / 2).[;

      then

       A1: ].( PI / 4), ( PI / 2).[ c= ( dom sec ) by Th1;

      assume

       A2: 1 < r & r < ( sqrt 2);

      then ( PI / 4) < ( arccosec2 r) & ( arccosec2 r) < ( PI / 2) by Th112;

      then x in ].( PI / 4), ( PI / 2).[;

      

      then ( sec . x) = (1 / ( cos . x)) by A1, RFUNCT_1:def 2

      .= (1 / (( sqrt ((r ^2 ) - 1)) / r)) by A2, Th116

      .= (r / ( sqrt ((r ^2 ) - 1))) by XCMPLX_1: 57;

      hence thesis;

    end;

    theorem :: SINCOS10:121

    

     Th121: arcsec1 is_differentiable_on ( sec .: ]. 0 , ( PI / 2).[)

    proof

      set X = ( sec .: ]. 0 , ( PI / 2).[);

      set g1 = ( arcsec1 | ( sec .: ]. 0 , ( PI / 2).[));

      set f = ( sec | [. 0 , ( PI / 2).[);

      set g = (f | ]. 0 , ( PI / 2).[);

      

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

      

       A2: ( dom ((g | ]. 0 , ( PI / 2).[) " )) = ( rng (g | ]. 0 , ( PI / 2).[)) by FUNCT_1: 33

      .= ( rng ( sec | ]. 0 , ( PI / 2).[)) by A1, RELAT_1: 72

      .= ( sec .: ]. 0 , ( PI / 2).[) by RELAT_1: 115;

      

       A3: ((g | ]. 0 , ( PI / 2).[) " ) = ((f | ]. 0 , ( PI / 2).[) " ) by RELAT_1: 72

      .= ( arcsec1 | (f .: ]. 0 , ( PI / 2).[)) by RFUNCT_2: 17

      .= ( arcsec1 | ( rng (f | ]. 0 , ( PI / 2).[))) by RELAT_1: 115

      .= ( arcsec1 | ( rng ( sec | ]. 0 , ( PI / 2).[))) by RELAT_1: 74, XXREAL_1: 22

      .= ( arcsec1 | ( sec .: ]. 0 , ( PI / 2).[)) by RELAT_1: 115;

      

       A4: g is_differentiable_on ]. 0 , ( PI / 2).[ by A1, Th5, FDIFF_2: 16;

      now

        

         A5: for x0 st x0 in ]. 0 , ( PI / 2).[ holds (( sin . x0) / (( cos . x0) ^2 )) > 0

        proof

          let x0;

          assume

           A6: x0 in ]. 0 , ( PI / 2).[;

           ]. 0 , ( PI / 2).[ c= ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 46;

          then

           A7: ( cos . x0) > 0 by A6, COMPTRIG: 11;

           ]. 0 , ( PI / 2).[ c= ]. 0 , PI .[ by COMPTRIG: 5, XXREAL_1: 46;

          then ( sin . x0) > 0 by A6, COMPTRIG: 7;

          hence thesis by A7;

        end;

        let x0 such that

         A8: x0 in ]. 0 , ( PI / 2).[;

        ( diff (g,x0)) = ((g `| ]. 0 , ( PI / 2).[) . x0) by A4, A8, FDIFF_1:def 7

        .= ((( sec | ]. 0 , ( PI / 2).[) `| ]. 0 , ( PI / 2).[) . x0) by RELAT_1: 74, XXREAL_1: 22

        .= (( sec `| ]. 0 , ( PI / 2).[) . x0) by Th5, FDIFF_2: 16

        .= ( diff ( sec ,x0)) by A8, Th5, FDIFF_1:def 7

        .= (( sin . x0) / (( cos . x0) ^2 )) by A8, Th5;

        hence ( diff (g,x0)) > 0 by A8, A5;

      end;

      then

       A9: g1 is_differentiable_on X by A2, A4, A3, Lm21, FDIFF_2: 48;

      

       A10: for x st x in X holds ( arcsec1 | X) is_differentiable_in x

      proof

        let x;

        assume x in X;

        then (g1 | X) is_differentiable_in x by A9, FDIFF_1:def 6;

        hence thesis by RELAT_1: 72;

      end;

      X c= ( dom arcsec1 ) by A2, A3, RELAT_1: 60;

      hence thesis by A10, FDIFF_1:def 6;

    end;

    theorem :: SINCOS10:122

    

     Th122: arcsec2 is_differentiable_on ( sec .: ].( PI / 2), PI .[)

    proof

      set X = ( sec .: ].( PI / 2), PI .[);

      set g1 = ( arcsec2 | ( sec .: ].( PI / 2), PI .[));

      set f = ( sec | ].( PI / 2), PI .]);

      set g = (f | ].( PI / 2), PI .[);

      

       A1: g = ( sec | ].( PI / 2), PI .[) by RELAT_1: 74, XXREAL_1: 21;

      

       A2: ( dom ((g | ].( PI / 2), PI .[) " )) = ( rng (g | ].( PI / 2), PI .[)) by FUNCT_1: 33

      .= ( rng ( sec | ].( PI / 2), PI .[)) by A1, RELAT_1: 72

      .= ( sec .: ].( PI / 2), PI .[) by RELAT_1: 115;

      

       A3: ((g | ].( PI / 2), PI .[) " ) = ((f | ].( PI / 2), PI .[) " ) by RELAT_1: 72

      .= ( arcsec2 | (f .: ].( PI / 2), PI .[)) by RFUNCT_2: 17

      .= ( arcsec2 | ( rng (f | ].( PI / 2), PI .[))) by RELAT_1: 115

      .= ( arcsec2 | ( rng ( sec | ].( PI / 2), PI .[))) by RELAT_1: 74, XXREAL_1: 21

      .= ( arcsec2 | ( sec .: ].( PI / 2), PI .[)) by RELAT_1: 115;

      

       A4: g is_differentiable_on ].( PI / 2), PI .[ by A1, Th6, FDIFF_2: 16;

      now

        

         A5: for x0 st x0 in ].( PI / 2), PI .[ holds (( sin . x0) / (( cos . x0) ^2 )) > 0

        proof

          let x0;

          assume

           A6: x0 in ].( PI / 2), PI .[;

           ].( PI / 2), PI .[ c= ].( PI / 2), ((3 / 2) * PI ).[ by COMPTRIG: 5, XXREAL_1: 46;

          then

           A7: ( cos . x0) < 0 by A6, COMPTRIG: 13;

           ].( PI / 2), PI .[ c= ]. 0 , PI .[ by XXREAL_1: 46;

          then ( sin . x0) > 0 by A6, COMPTRIG: 7;

          hence thesis by A7;

        end;

        let x0 such that

         A8: x0 in ].( PI / 2), PI .[;

        ( diff (g,x0)) = ((g `| ].( PI / 2), PI .[) . x0) by A4, A8, FDIFF_1:def 7

        .= ((( sec | ].( PI / 2), PI .[) `| ].( PI / 2), PI .[) . x0) by RELAT_1: 74, XXREAL_1: 21

        .= (( sec `| ].( PI / 2), PI .[) . x0) by Th6, FDIFF_2: 16

        .= ( diff ( sec ,x0)) by A8, Th6, FDIFF_1:def 7

        .= (( sin . x0) / (( cos . x0) ^2 )) by A8, Th6;

        hence ( diff (g,x0)) > 0 by A8, A5;

      end;

      then

       A9: g1 is_differentiable_on X by A2, A4, A3, Lm22, FDIFF_2: 48;

      

       A10: for x st x in X holds ( arcsec2 | X) is_differentiable_in x

      proof

        let x;

        assume x in X;

        then (g1 | X) is_differentiable_in x by A9, FDIFF_1:def 6;

        hence thesis by RELAT_1: 72;

      end;

      X c= ( dom arcsec2 ) by A2, A3, RELAT_1: 60;

      hence thesis by A10, FDIFF_1:def 6;

    end;

    theorem :: SINCOS10:123

    

     Th123: arccosec1 is_differentiable_on ( cosec .: ].( - ( PI / 2)), 0 .[)

    proof

      set X = ( cosec .: ].( - ( PI / 2)), 0 .[);

      set g1 = ( arccosec1 | ( cosec .: ].( - ( PI / 2)), 0 .[));

      set f = ( cosec | [.( - ( PI / 2)), 0 .[);

      set g = (f | ].( - ( PI / 2)), 0 .[);

      

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

      

       A2: ( dom ((g | ].( - ( PI / 2)), 0 .[) " )) = ( rng (g | ].( - ( PI / 2)), 0 .[)) by FUNCT_1: 33

      .= ( rng ( cosec | ].( - ( PI / 2)), 0 .[)) by A1, RELAT_1: 72

      .= ( cosec .: ].( - ( PI / 2)), 0 .[) by RELAT_1: 115;

      

       A3: ((g | ].( - ( PI / 2)), 0 .[) " ) = ((f | ].( - ( PI / 2)), 0 .[) " ) by RELAT_1: 72

      .= ( arccosec1 | (f .: ].( - ( PI / 2)), 0 .[)) by RFUNCT_2: 17

      .= ( arccosec1 | ( rng (f | ].( - ( PI / 2)), 0 .[))) by RELAT_1: 115

      .= ( arccosec1 | ( rng ( cosec | ].( - ( PI / 2)), 0 .[))) by RELAT_1: 74, XXREAL_1: 22

      .= ( arccosec1 | ( cosec .: ].( - ( PI / 2)), 0 .[)) by RELAT_1: 115;

      

       A4: g is_differentiable_on ].( - ( PI / 2)), 0 .[ by A1, Th7, FDIFF_2: 16;

      now

        

         A5: for x0 st x0 in ].( - ( PI / 2)), 0 .[ holds ( - (( cos . x0) / (( sin . x0) ^2 ))) < 0

        proof

          let x0;

          assume

           A6: x0 in ].( - ( PI / 2)), 0 .[;

          then x0 < 0 by XXREAL_1: 4;

          then

           A7: (x0 + (2 * PI )) < ( 0 + (2 * PI )) by XREAL_1: 8;

          ( ].( - ( PI / 2)), 0 .[ \/ {( - ( PI / 2))}) = [.( - ( PI / 2)), 0 .[ by XXREAL_1: 131;

          then ].( - ( PI / 2)), 0 .[ c= [.( - ( PI / 2)), 0 .[ by XBOOLE_1: 7;

          then ].( - ( PI / 2)), 0 .[ c= ].( - PI ), 0 .[ by Lm3;

          then ( - PI ) < x0 by A6, XXREAL_1: 4;

          then (( - PI ) + (2 * PI )) < (x0 + (2 * PI )) by XREAL_1: 8;

          then (x0 + (2 * PI )) in ]. PI , (2 * PI ).[ by A7;

          then ( sin . (x0 + (2 * PI ))) < 0 by COMPTRIG: 9;

          then

           A8: ( sin . x0) < 0 by SIN_COS: 78;

           ].( - ( PI / 2)), 0 .[ c= ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 46;

          then ( cos . x0) > 0 by A6, COMPTRIG: 11;

          hence thesis by A8;

        end;

        let x0 such that

         A9: x0 in ].( - ( PI / 2)), 0 .[;

        ( diff (g,x0)) = ((g `| ].( - ( PI / 2)), 0 .[) . x0) by A4, A9, FDIFF_1:def 7

        .= ((( cosec | ].( - ( PI / 2)), 0 .[) `| ].( - ( PI / 2)), 0 .[) . x0) by RELAT_1: 74, XXREAL_1: 22

        .= (( cosec `| ].( - ( PI / 2)), 0 .[) . x0) by Th7, FDIFF_2: 16

        .= ( diff ( cosec ,x0)) by A9, Th7, FDIFF_1:def 7

        .= ( - (( cos . x0) / (( sin . x0) ^2 ))) by A9, Th7;

        hence ( diff (g,x0)) < 0 by A9, A5;

      end;

      then

       A10: g1 is_differentiable_on X by A2, A4, A3, Lm23, FDIFF_2: 48;

      

       A11: for x st x in X holds ( arccosec1 | X) is_differentiable_in x

      proof

        let x;

        assume x in X;

        then (g1 | X) is_differentiable_in x by A10, FDIFF_1:def 6;

        hence thesis by RELAT_1: 72;

      end;

      X c= ( dom arccosec1 ) by A2, A3, RELAT_1: 60;

      hence thesis by A11, FDIFF_1:def 6;

    end;

    theorem :: SINCOS10:124

    

     Th124: arccosec2 is_differentiable_on ( cosec .: ]. 0 , ( PI / 2).[)

    proof

      set X = ( cosec .: ]. 0 , ( PI / 2).[);

      set g1 = ( arccosec2 | ( cosec .: ]. 0 , ( PI / 2).[));

      set f = ( cosec | ]. 0 , ( PI / 2).]);

      set g = (f | ]. 0 , ( PI / 2).[);

      

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

      

       A2: ( dom ((g | ]. 0 , ( PI / 2).[) " )) = ( rng (g | ]. 0 , ( PI / 2).[)) by FUNCT_1: 33

      .= ( rng ( cosec | ]. 0 , ( PI / 2).[)) by A1, RELAT_1: 72

      .= ( cosec .: ]. 0 , ( PI / 2).[) by RELAT_1: 115;

      

       A3: ((g | ]. 0 , ( PI / 2).[) " ) = ((f | ]. 0 , ( PI / 2).[) " ) by RELAT_1: 72

      .= ( arccosec2 | (f .: ]. 0 , ( PI / 2).[)) by RFUNCT_2: 17

      .= ( arccosec2 | ( rng (f | ]. 0 , ( PI / 2).[))) by RELAT_1: 115

      .= ( arccosec2 | ( rng ( cosec | ]. 0 , ( PI / 2).[))) by RELAT_1: 74, XXREAL_1: 21

      .= ( arccosec2 | ( cosec .: ]. 0 , ( PI / 2).[)) by RELAT_1: 115;

      

       A4: g is_differentiable_on ]. 0 , ( PI / 2).[ by A1, Th8, FDIFF_2: 16;

      now

        

         A5: for x0 st x0 in ]. 0 , ( PI / 2).[ holds ( - (( cos . x0) / (( sin . x0) ^2 ))) < 0

        proof

          let x0;

          assume

           A6: x0 in ]. 0 , ( PI / 2).[;

           ]. 0 , ( PI / 2).[ c= ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 46;

          then

           A7: ( cos . x0) > 0 by A6, COMPTRIG: 11;

           ]. 0 , ( PI / 2).[ c= ]. 0 , PI .[ by COMPTRIG: 5, XXREAL_1: 46;

          then ( sin . x0) > 0 by A6, COMPTRIG: 7;

          hence thesis by A7;

        end;

        let x0 such that

         A8: x0 in ]. 0 , ( PI / 2).[;

        ( diff (g,x0)) = ((g `| ]. 0 , ( PI / 2).[) . x0) by A4, A8, FDIFF_1:def 7

        .= ((( cosec | ]. 0 , ( PI / 2).[) `| ]. 0 , ( PI / 2).[) . x0) by RELAT_1: 74, XXREAL_1: 21

        .= (( cosec `| ]. 0 , ( PI / 2).[) . x0) by Th8, FDIFF_2: 16

        .= ( diff ( cosec ,x0)) by A8, Th8, FDIFF_1:def 7

        .= ( - (( cos . x0) / (( sin . x0) ^2 ))) by A8, Th8;

        hence ( diff (g,x0)) < 0 by A8, A5;

      end;

      then

       A9: g1 is_differentiable_on X by A2, A4, A3, Lm24, FDIFF_2: 48;

      

       A10: for x st x in X holds ( arccosec2 | X) is_differentiable_in x

      proof

        let x;

        assume x in X;

        then (g1 | X) is_differentiable_in x by A9, FDIFF_1:def 6;

        hence thesis by RELAT_1: 72;

      end;

      X c= ( dom arccosec2 ) by A2, A3, RELAT_1: 60;

      hence thesis by A10, FDIFF_1:def 6;

    end;

    theorem :: SINCOS10:125

    ( sec .: ]. 0 , ( PI / 2).[) is open

    proof

      for x0 st x0 in ]. 0 , ( PI / 2).[ holds ( diff ( sec ,x0)) > 0

      proof

        let x0;

        assume

         A1: x0 in ]. 0 , ( PI / 2).[;

         ]. 0 , ( PI / 2).[ c= ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 46;

        then

         A2: ( cos . x0) > 0 by A1, COMPTRIG: 11;

         ]. 0 , ( PI / 2).[ c= ]. 0 , PI .[ by COMPTRIG: 5, XXREAL_1: 46;

        then ( sin . x0) > 0 by A1, COMPTRIG: 7;

        then (( sin . x0) / (( cos . x0) ^2 )) > ( 0 / (( cos . x0) ^2 )) by A2;

        hence thesis by A1, Th5;

      end;

      then ( rng ( sec | ]. 0 , ( PI / 2).[)) is open by Lm10, Th5, FDIFF_2: 41;

      hence thesis by RELAT_1: 115;

    end;

    theorem :: SINCOS10:126

    ( sec .: ].( PI / 2), PI .[) is open

    proof

      for x0 st x0 in ].( PI / 2), PI .[ holds ( diff ( sec ,x0)) > 0

      proof

        let x0;

        assume

         A1: x0 in ].( PI / 2), PI .[;

         ].( PI / 2), PI .[ c= ].( PI / 2), ((3 / 2) * PI ).[ by COMPTRIG: 5, XXREAL_1: 46;

        then

         A2: ( cos . x0) < 0 by A1, COMPTRIG: 13;

         ].( PI / 2), PI .[ c= ]. 0 , PI .[ by XXREAL_1: 46;

        then ( sin . x0) > 0 by A1, COMPTRIG: 7;

        then (( sin . x0) / (( cos . x0) ^2 )) > ( 0 / (( cos . x0) ^2 )) by A2;

        hence thesis by A1, Th6;

      end;

      then ( rng ( sec | ].( PI / 2), PI .[)) is open by Lm12, Th6, FDIFF_2: 41;

      hence thesis by RELAT_1: 115;

    end;

    theorem :: SINCOS10:127

    ( cosec .: ].( - ( PI / 2)), 0 .[) is open

    proof

      for x0 st x0 in ].( - ( PI / 2)), 0 .[ holds ( diff ( cosec ,x0)) < 0

      proof

        let x0;

        assume

         A1: x0 in ].( - ( PI / 2)), 0 .[;

        then x0 < 0 by XXREAL_1: 4;

        then

         A2: (x0 + (2 * PI )) < ( 0 + (2 * PI )) by XREAL_1: 8;

        ( ].( - ( PI / 2)), 0 .[ \/ {( - ( PI / 2))}) = [.( - ( PI / 2)), 0 .[ by XXREAL_1: 131;

        then ].( - ( PI / 2)), 0 .[ c= [.( - ( PI / 2)), 0 .[ by XBOOLE_1: 7;

        then ].( - ( PI / 2)), 0 .[ c= ].( - PI ), 0 .[ by Lm3;

        then ( - PI ) < x0 by A1, XXREAL_1: 4;

        then (( - PI ) + (2 * PI )) < (x0 + (2 * PI )) by XREAL_1: 8;

        then (x0 + (2 * PI )) in ]. PI , (2 * PI ).[ by A2;

        then ( sin . (x0 + (2 * PI ))) < 0 by COMPTRIG: 9;

        then

         A3: ( sin . x0) < 0 by SIN_COS: 78;

         ].( - ( PI / 2)), 0 .[ c= ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 46;

        then ( cos . x0) > 0 by A1, COMPTRIG: 11;

        then ( - (( cos . x0) / (( sin . x0) ^2 ))) < ( - 0 ) by A3;

        hence thesis by A1, Th7;

      end;

      then ( rng ( cosec | ].( - ( PI / 2)), 0 .[)) is open by Lm16, Th7, FDIFF_2: 41;

      hence thesis by RELAT_1: 115;

    end;

    theorem :: SINCOS10:128

    ( cosec .: ]. 0 , ( PI / 2).[) is open

    proof

      for x0 st x0 in ]. 0 , ( PI / 2).[ holds ( diff ( cosec ,x0)) < 0

      proof

        let x0;

        assume

         A1: x0 in ]. 0 , ( PI / 2).[;

         ]. 0 , ( PI / 2).[ c= ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 46;

        then

         A2: ( cos . x0) > 0 by A1, COMPTRIG: 11;

         ]. 0 , ( PI / 2).[ c= ]. 0 , PI .[ by COMPTRIG: 5, XXREAL_1: 46;

        then ( sin . x0) > 0 by A1, COMPTRIG: 7;

        then ( - (( cos . x0) / (( sin . x0) ^2 ))) < ( - 0 ) by A2;

        hence thesis by A1, Th8;

      end;

      then ( rng ( cosec | ]. 0 , ( PI / 2).[)) is open by Lm18, Th8, FDIFF_2: 41;

      hence thesis by RELAT_1: 115;

    end;

    theorem :: SINCOS10:129

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

    theorem :: SINCOS10:130

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

    theorem :: SINCOS10:131

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

    theorem :: SINCOS10:132

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