jordan23.miz



    begin

    reserve n for Nat;

    theorem :: JORDAN23:1

    

     Th1: for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) holds ( len ( L_Cut (f,p))) >= 1

    proof

      let f be FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2);

      assume p in ( L~ f);

      then ( L_Cut (f,p)) <> {} by JORDAN1E: 3;

      then

       A1: ( len ( L_Cut (f,p))) > 0 by NAT_1: 3;

      1 = ( 0 + 1);

      hence thesis by A1, NAT_1: 13;

    end;

    theorem :: JORDAN23:2

    for f be non empty FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) holds ( len ( R_Cut (f,p))) >= 1

    proof

      let f be non empty FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2);

      ( R_Cut (f,p)) <> {} by JORDAN1J: 44;

      then

       A1: ( len ( R_Cut (f,p))) > 0 by NAT_1: 3;

      1 = ( 0 + 1);

      hence thesis by A1, NAT_1: 13;

    end;

    theorem :: JORDAN23:3

    

     Th3: for f be FinSequence of ( TOP-REAL 2) holds for p,q be Point of ( TOP-REAL 2) holds ( B_Cut (f,p,q)) <> {}

    proof

      let f be FinSequence of ( TOP-REAL 2);

      let p,q be Point of ( TOP-REAL 2);

      

       A1: ( R_Cut (( L_Cut (f,q)),p)) <> {} by JORDAN1J: 44;

      per cases ;

        suppose p in ( L~ f) & q in ( L~ f) & ( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

        then ( B_Cut (f,p,q)) = ( R_Cut (( L_Cut (f,p)),q)) by JORDAN3:def 7;

        hence thesis by JORDAN1J: 44;

      end;

        suppose not (p in ( L~ f) & q in ( L~ f) & ( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

        then ( B_Cut (f,p,q)) = ( Rev ( R_Cut (( L_Cut (f,q)),p))) by JORDAN3:def 7;

        hence thesis by A1;

      end;

    end;

    registration

      let x be set;

      cluster <*x*> -> one-to-one;

      coherence by FINSEQ_3: 93;

    end

    definition

      let f be FinSequence;

      :: JORDAN23:def1

      attr f is almost-one-to-one means for i,j be Nat st i in ( dom f) & j in ( dom f) & (i <> 1 or j <> ( len f)) & (i <> ( len f) or j <> 1) & (f . i) = (f . j) holds i = j;

    end

    definition

      let f be FinSequence;

      :: JORDAN23:def2

      attr f is weakly-one-to-one means for i be Nat st 1 <= i & i < ( len f) holds (f . i) <> (f . (i + 1));

    end

    definition

      let f be FinSequence;

      :: JORDAN23:def3

      attr f is poorly-one-to-one means

      : Def3: for i be Nat st 1 <= i & i < ( len f) holds (f . i) <> (f . (i + 1)) if ( len f) <> 2

      otherwise not contradiction;

      consistency ;

    end

    theorem :: JORDAN23:4

    for D be set holds for f be FinSequence of D holds f is almost-one-to-one iff for i,j be Nat st i in ( dom f) & j in ( dom f) & (i <> 1 or j <> ( len f)) & (i <> ( len f) or j <> 1) & (f /. i) = (f /. j) holds i = j

    proof

      let D be set;

      let f be FinSequence of D;

      thus f is almost-one-to-one implies for i,j be Nat st i in ( dom f) & j in ( dom f) & (i <> 1 or j <> ( len f)) & (i <> ( len f) or j <> 1) & (f /. i) = (f /. j) holds i = j

      proof

        assume

         A1: f is almost-one-to-one;

        let i,j be Nat such that

         A2: i in ( dom f) and

         A3: j in ( dom f) and

         A4: i <> 1 or j <> ( len f) and

         A5: i <> ( len f) or j <> 1 and

         A6: (f /. i) = (f /. j);

        (f . i) = (f /. j) by A2, A6, PARTFUN1:def 6

        .= (f . j) by A3, PARTFUN1:def 6;

        hence thesis by A1, A2, A3, A4, A5;

      end;

      assume

       A7: for i,j be Nat st i in ( dom f) & j in ( dom f) & (i <> 1 or j <> ( len f)) & (i <> ( len f) or j <> 1) & (f /. i) = (f /. j) holds i = j;

      now

        let i,j be Nat such that

         A8: i in ( dom f) and

         A9: j in ( dom f) and

         A10: i <> 1 or j <> ( len f) and

         A11: i <> ( len f) or j <> 1 and

         A12: (f . i) = (f . j);

        (f /. i) = (f . j) by A8, A12, PARTFUN1:def 6

        .= (f /. j) by A9, PARTFUN1:def 6;

        hence i = j by A7, A8, A9, A10, A11;

      end;

      hence thesis;

    end;

    theorem :: JORDAN23:5

    

     Th5: for D be set holds for f be FinSequence of D holds f is weakly-one-to-one iff for i be Nat st 1 <= i & i < ( len f) holds (f /. i) <> (f /. (i + 1))

    proof

      let D be set;

      let f be FinSequence of D;

      thus f is weakly-one-to-one implies for i be Nat st 1 <= i & i < ( len f) holds (f /. i) <> (f /. (i + 1))

      proof

        assume

         A1: f is weakly-one-to-one;

        let i be Nat such that

         A2: 1 <= i and

         A3: i < ( len f);

        

         A4: (i + 1) <= ( len f) by A3, NAT_1: 13;

        1 < (i + 1) by A2, NAT_1: 13;

        then

         A5: (f . (i + 1)) = (f /. (i + 1)) by A4, FINSEQ_4: 15;

        (f . i) = (f /. i) by A2, A3, FINSEQ_4: 15;

        hence thesis by A1, A2, A3, A5;

      end;

      assume

       A6: for i be Nat st 1 <= i & i < ( len f) holds (f /. i) <> (f /. (i + 1));

      now

        let i be Nat such that

         A7: 1 <= i and

         A8: i < ( len f);

        

         A9: (i + 1) <= ( len f) by A8, NAT_1: 13;

        1 < (i + 1) by A7, NAT_1: 13;

        then

         A10: (f . (i + 1)) = (f /. (i + 1)) by A9, FINSEQ_4: 15;

        (f . i) = (f /. i) by A7, A8, FINSEQ_4: 15;

        hence (f . i) <> (f . (i + 1)) by A6, A7, A8, A10;

      end;

      hence thesis;

    end;

    theorem :: JORDAN23:6

    for D be set holds for f be FinSequence of D holds f is poorly-one-to-one iff (( len f) <> 2 implies for i be Nat st 1 <= i & i < ( len f) holds (f /. i) <> (f /. (i + 1)))

    proof

      let D be set;

      let f be FinSequence of D;

      thus f is poorly-one-to-one & ( len f) <> 2 implies for i be Nat st 1 <= i & i < ( len f) holds (f /. i) <> (f /. (i + 1))

      proof

        assume that

         A1: f is poorly-one-to-one and

         A2: ( len f) <> 2;

        let i be Nat such that

         A3: 1 <= i and

         A4: i < ( len f);

        

         A5: (i + 1) <= ( len f) by A4, NAT_1: 13;

        1 < (i + 1) by A3, NAT_1: 13;

        then

         A6: (f . (i + 1)) = (f /. (i + 1)) by A5, FINSEQ_4: 15;

        (f . i) = (f /. i) by A3, A4, FINSEQ_4: 15;

        hence thesis by A1, A2, A3, A4, A6, Def3;

      end;

      assume

       A7: ( len f) <> 2 implies for i be Nat st 1 <= i & i < ( len f) holds (f /. i) <> (f /. (i + 1));

      per cases ;

        suppose

         A8: ( len f) <> 2;

        now

          let i be Nat such that

           A9: 1 <= i and

           A10: i < ( len f);

          

           A11: (i + 1) <= ( len f) by A10, NAT_1: 13;

          1 < (i + 1) by A9, NAT_1: 13;

          then

           A12: (f . (i + 1)) = (f /. (i + 1)) by A11, FINSEQ_4: 15;

          (f . i) = (f /. i) by A9, A10, FINSEQ_4: 15;

          hence (f . i) <> (f . (i + 1)) by A7, A8, A9, A10, A12;

        end;

        hence thesis by A8, Def3;

      end;

        suppose ( len f) = 2;

        hence thesis by Def3;

      end;

    end;

    registration

      cluster one-to-one -> almost-one-to-one for FinSequence;

      coherence ;

    end

    registration

      cluster almost-one-to-one -> poorly-one-to-one for FinSequence;

      coherence

      proof

        let f be FinSequence;

        assume

         A1: f is almost-one-to-one;

        per cases ;

          case

           A2: ( len f) <> 2;

          now

            per cases ;

              suppose

               A3: ( len f) <> 0 ;

              let i be Nat;

              

               A4: not (i = ( len f) & (i + 1) = 1) by A3;

              

               A5: (i + 1) >= 1 by NAT_1: 11;

              assume that

               A6: 1 <= i and

               A7: i < ( len f);

              (i + 1) <= ( len f) by A7, NAT_1: 13;

              then

               A8: (i + 1) in ( dom f) by A5, FINSEQ_3: 25;

              

               A9: not (i = 1 & (i + 1) = ( len f)) by A2;

              

               A10: i <> (i + 1);

              i in ( dom f) by A6, A7, FINSEQ_3: 25;

              hence (f . i) <> (f . (i + 1)) by A1, A8, A10, A9, A4;

            end;

              suppose

               A11: ( len f) = 0 ;

              let i be Nat;

              assume that

               A12: 1 <= i and

               A13: i < ( len f);

              thus (f . i) <> (f . (i + 1)) by A11, A12, A13;

            end;

          end;

          hence thesis;

        end;

          case ( len f) = 2;

        end;

      end;

    end

    theorem :: JORDAN23:7

    

     Th7: for f be FinSequence st ( len f) <> 2 holds f is weakly-one-to-one iff f is poorly-one-to-one by Def3;

    registration

      cluster empty -> weakly-one-to-one for FinSequence;

      coherence ;

    end

    registration

      let x be set;

      cluster <*x*> -> weakly-one-to-one;

      coherence by FINSEQ_1: 39;

    end

    registration

      let x,y be set;

      cluster <*x, y*> -> poorly-one-to-one;

      coherence

      proof

        ( len <*x, y*>) = 2 by FINSEQ_1: 44;

        hence thesis by Def3;

      end;

    end

    registration

      cluster weakly-one-to-one non empty for FinSequence;

      existence

      proof

        set x = the set;

        ( len <*x*>) <> 2 by FINSEQ_1: 39;

        hence thesis;

      end;

    end

    registration

      let D be non empty set;

      cluster weakly-one-to-one circular non empty for FinSequence of D;

      existence

      proof

        set x = the Element of D;

        ( <*x*> /. 1) = ( <*x*> /. ( len <*x*>)) by FINSEQ_1: 39;

        then <*x*> is circular by FINSEQ_6:def 1;

        hence thesis;

      end;

    end

    theorem :: JORDAN23:8

    

     Th8: for f be FinSequence st f is almost-one-to-one holds ( Rev f) is almost-one-to-one

    proof

      let f be FinSequence;

      assume

       A1: f is almost-one-to-one;

      let i,j be Nat;

      assume that

       A2: i in ( dom ( Rev f)) and

       A3: j in ( dom ( Rev f)) and

       A4: i <> 1 or j <> ( len ( Rev f)) and

       A5: i <> ( len ( Rev f)) or j <> 1 and

       A6: (( Rev f) . i) = (( Rev f) . j);

      

       A7: not (((( len f) - i) + 1) = ( len f) & ((( len f) - j) + 1) = 1) by A4, FINSEQ_5:def 3;

      

       A8: ( dom f) = ( dom ( Rev f)) by FINSEQ_5: 57;

      then i in ( Seg ( len f)) by A2, FINSEQ_1:def 3;

      then ((( len f) - i) + 1) in ( Seg ( len f)) by FINSEQ_5: 2;

      then

       A9: ((( len f) - i) + 1) in ( dom f) by FINSEQ_1:def 3;

      

       A10: (( Rev f) . j) = (f . ((( len f) - j) + 1)) by A3, FINSEQ_5:def 3;

      

       A11: (( Rev f) . i) = (f . ((( len f) - i) + 1)) by A2, FINSEQ_5:def 3;

      j in ( Seg ( len f)) by A3, A8, FINSEQ_1:def 3;

      then ((( len f) - j) + 1) in ( Seg ( len f)) by FINSEQ_5: 2;

      then

       A12: ((( len f) - j) + 1) in ( dom f) by FINSEQ_1:def 3;

       not (((( len f) - i) + 1) = 1 & ((( len f) - j) + 1) = ( len f)) by A5, FINSEQ_5:def 3;

      then ((( len f) - i) + 1) = ((( len f) - j) + 1) by A1, A6, A9, A12, A7, A11, A10;

      hence thesis;

    end;

    theorem :: JORDAN23:9

    

     Th9: for f be FinSequence st f is weakly-one-to-one holds ( Rev f) is weakly-one-to-one

    proof

      let f be FinSequence;

      assume

       A1: f is weakly-one-to-one;

      

       A2: ( len f) = ( len ( Rev f)) by FINSEQ_5:def 3;

      let i be Nat;

      assume that

       A3: 1 <= i and

       A4: i < ( len ( Rev f));

      

       A5: (i + 1) <= ( len ( Rev f)) by A4, NAT_1: 13;

      (i + 1) >= 1 by NAT_1: 11;

      then

       A6: (i + 1) in ( Seg ( len ( Rev f))) by A5, FINSEQ_1: 1;

      then (i + 1) in ( dom ( Rev f)) by FINSEQ_1:def 3;

      then

       A7: (( Rev f) . (i + 1)) = (f . ((( len f) - (i + 1)) + 1)) by FINSEQ_5:def 3;

      

       A8: i in ( Seg ( len ( Rev f))) by A3, A4, FINSEQ_1: 1;

      then i in ( dom ( Rev f)) by FINSEQ_1:def 3;

      then

       A9: (( Rev f) . i) = (f . ((( len f) - i) + 1)) by FINSEQ_5:def 3;

      ((( len f) - (i + 1)) + 1) = (( len f) - i);

      then

      reconsider j = (( len f) - i) as Nat by A2, A5, FINSEQ_5: 1;

      ((( len f) - i) + 1) in ( Seg ( len f)) by A2, A8, FINSEQ_5: 2;

      then (j + 1) <= ( len f) by FINSEQ_1: 1;

      then

       A10: j < ( len f) by NAT_1: 13;

      ((( len f) - (i + 1)) + 1) in ( Seg ( len f)) by A2, A6, FINSEQ_5: 2;

      then j >= 1 by FINSEQ_1: 1;

      hence thesis by A1, A9, A7, A10;

    end;

    theorem :: JORDAN23:10

    

     Th10: for f be FinSequence st f is poorly-one-to-one holds ( Rev f) is poorly-one-to-one

    proof

      let f be FinSequence;

      assume

       A1: f is poorly-one-to-one;

      

       A2: ( len f) = ( len ( Rev f)) by FINSEQ_5:def 3;

      per cases ;

        suppose

         A3: ( len f) <> 2;

        then f is weakly-one-to-one by A1, Th7;

        then ( Rev f) is weakly-one-to-one by Th9;

        hence thesis by A2, A3, Th7;

      end;

        suppose ( len f) = 2;

        hence thesis by A2, Def3;

      end;

    end;

    registration

      cluster one-to-one non empty for FinSequence;

      existence

      proof

        set x = the set;

         <*x*> is non empty one-to-one;

        hence thesis;

      end;

    end

    registration

      let f be almost-one-to-one FinSequence;

      cluster ( Rev f) -> almost-one-to-one;

      coherence by Th8;

    end

    registration

      let f be weakly-one-to-one FinSequence;

      cluster ( Rev f) -> weakly-one-to-one;

      coherence by Th9;

    end

    registration

      let f be poorly-one-to-one FinSequence;

      cluster ( Rev f) -> poorly-one-to-one;

      coherence by Th10;

    end

    theorem :: JORDAN23:11

    

     Th11: for D be non empty set holds for f be FinSequence of D st f is almost-one-to-one holds for p be Element of D holds ( Rotate (f,p)) is almost-one-to-one

    proof

      let D be non empty set;

      let f be FinSequence of D;

      assume

       A1: f is almost-one-to-one;

      let p be Element of D;

      per cases ;

        suppose

         A2: p in ( rng f);

        then ( 0 + 1) <= (p .. f) by FINSEQ_4: 21;

        then

         A3: ((p .. f) - 1) >= 0 by XREAL_1: 19;

        

         A4: ( len (f :- p)) = ((( len f) - (p .. f)) + 1) by A2, FINSEQ_5: 50;

        let i,j be Nat;

        assume that

         A5: i in ( dom ( Rotate (f,p))) and

         A6: j in ( dom ( Rotate (f,p))) and

         A7: i <> 1 or j <> ( len ( Rotate (f,p))) and

         A8: i <> ( len ( Rotate (f,p))) or j <> 1 and

         A9: (( Rotate (f,p)) . i) = (( Rotate (f,p)) . j);

        

         A10: ( 0 + 1) <= i by A5, FINSEQ_3: 25;

        

         A11: ( dom ( Rotate (f,p))) = ( dom f) by FINSEQ_6: 180;

        then

         A12: i <= ( len f) by A5, FINSEQ_3: 25;

        then

         A13: (i - ( len f)) <= (( len f) - ( len f)) by XREAL_1: 9;

        

         A14: j <= ( len f) by A6, A11, FINSEQ_3: 25;

        then

         A15: (j - ( len f)) <= (( len f) - ( len f)) by XREAL_1: 9;

        

         A16: ( len ( Rotate (f,p))) = ( len f) by FINSEQ_6: 179;

        

         A17: ( 0 + 1) <= j by A6, FINSEQ_3: 25;

        then

         A18: (j - 1) >= 0 by XREAL_1: 19;

         A19:

        now

          assume that

           A20: ((i -' 1) + (p .. f)) = ( len f) and

           A21: ((j -' 1) + (p .. f)) = 1;

          ((j -' 1) + ((p .. f) - 1)) = 0 by A21;

          then

           A22: (j -' 1) = 0 by A3;

          then (j - 1) = 0 by A18, XREAL_0:def 2;

          hence contradiction by A8, A16, A10, A20, A21, A22, XREAL_1: 235;

        end;

        

         A23: (p .. f) <= ( len f) by A2, FINSEQ_4: 21;

        

         A24: (i - 1) >= 0 by A10, XREAL_1: 19;

         A25:

        now

          assume that

           A26: ((i -' 1) + (p .. f)) = 1 and

           A27: ((j -' 1) + (p .. f)) = ( len f);

          ((i -' 1) + ((p .. f) - 1)) = 0 by A26;

          then

           A28: (i -' 1) = 0 by A3;

          then (i - 1) = 0 by A24, XREAL_0:def 2;

          hence contradiction by A7, A16, A17, A26, A27, A28, XREAL_1: 235;

        end;

        now

          per cases ;

            suppose

             A29: i <= ( len (f :- p));

            then i in ( dom (f :- p)) by A10, FINSEQ_3: 25;

            then ((i -' 1) + 1) in ( dom (f :- p)) by A10, XREAL_1: 235;

            then

             A30: ((i -' 1) + (p .. f)) in ( dom f) by A2, FINSEQ_5: 51;

            (( Rotate (f,p)) /. i) = (f /. ((i -' 1) + (p .. f))) by A2, A10, A29, FINSEQ_6: 174;

            then

             A31: (( Rotate (f,p)) . i) = (f /. ((i -' 1) + (p .. f))) by A5, PARTFUN1:def 6;

            now

              per cases ;

                suppose

                 A32: j <= ( len (f :- p));

                then j in ( dom (f :- p)) by A17, FINSEQ_3: 25;

                then ((j -' 1) + 1) in ( dom (f :- p)) by A17, XREAL_1: 235;

                then

                 A33: ((j -' 1) + (p .. f)) in ( dom f) by A2, FINSEQ_5: 51;

                (( Rotate (f,p)) /. j) = (f /. ((j -' 1) + (p .. f))) by A2, A17, A32, FINSEQ_6: 174;

                then

                 A34: (f /. ((i -' 1) + (p .. f))) = (f /. ((j -' 1) + (p .. f))) by A6, A9, A31, PARTFUN1:def 6;

                (f . ((i -' 1) + (p .. f))) = (f /. ((i -' 1) + (p .. f))) by A30, PARTFUN1:def 6

                .= (f . ((j -' 1) + (p .. f))) by A34, A33, PARTFUN1:def 6;

                then ((i -' 1) + (p .. f)) = ((j -' 1) + (p .. f)) by A1, A25, A19, A30, A33;

                hence thesis by A10, A17, XREAL_1: 234;

              end;

                suppose

                 A35: j > ( len (f :- p));

                then (( Rotate (f,p)) /. j) = (f /. ((j + (p .. f)) -' ( len f))) by A2, A14, FINSEQ_6: 177;

                then

                 A36: (f /. ((i -' 1) + (p .. f))) = (f /. ((j + (p .. f)) -' ( len f))) by A6, A9, A31, PARTFUN1:def 6;

                

                 A37: (j - (( len f) - (p .. f))) > 1 by A4, A35, XREAL_1: 20;

                then

                 A38: ((j + (p .. f)) - ( len f)) > 1;

                then

                 A39: ((j + (p .. f)) -' ( len f)) >= 1 by XREAL_0:def 2;

                (j + (p .. f)) <= (( len f) + ( len f)) by A23, A14, XREAL_1: 7;

                then ((j + (p .. f)) - ( len f)) <= ( len f) by XREAL_1: 20;

                then ((j + (p .. f)) -' ( len f)) <= ( len f) by A37, XREAL_0:def 2;

                then

                 A40: ((j + (p .. f)) -' ( len f)) in ( dom f) by A39, FINSEQ_3: 25;

                 A41:

                now

                  assume that

                   A42: ((i -' 1) + (p .. f)) = 1 and

                   A43: ((j + (p .. f)) -' ( len f)) = ( len f);

                  ((j + (p .. f)) - ( len f)) = ( len f) by A37, A43, XREAL_0:def 2;

                  then (j + (p .. f)) = (( len f) + ( len f));

                  then

                   A44: j >= ( len f) by A23, XREAL_1: 8;

                  ((i -' 1) + ((p .. f) - 1)) = 0 by A42;

                  then (i -' 1) = 0 by A3;

                  then (i - 1) = 0 by A24, XREAL_0:def 2;

                  hence contradiction by A7, A16, A14, A44, XXREAL_0: 1;

                end;

                

                 A45: ((i -' 1) + (p .. f)) <> ( len f) or ((j + (p .. f)) -' ( len f)) <> 1 by A38, XREAL_0:def 2;

                (f . ((i -' 1) + (p .. f))) = (f /. ((i -' 1) + (p .. f))) by A30, PARTFUN1:def 6

                .= (f . ((j + (p .. f)) -' ( len f))) by A36, A40, PARTFUN1:def 6;

                then ((i -' 1) + (p .. f)) = ((j + (p .. f)) -' ( len f)) by A1, A30, A41, A45, A40;

                then

                 A46: ((i -' 1) + (p .. f)) = ((j + (p .. f)) - ( len f)) by A37, XREAL_0:def 2;

                then

                 A47: (j - ( len f)) = 0 by A15;

                (i - 1) = 0 by A24, A15, A46, XREAL_0:def 2;

                hence thesis by A7, A47, FINSEQ_6: 179;

              end;

            end;

            hence thesis;

          end;

            suppose

             A48: i > ( len (f :- p));

            then

             A49: (i - (( len f) - (p .. f))) > 1 by A4, XREAL_1: 20;

            (i + (p .. f)) <= (( len f) + ( len f)) by A23, A12, XREAL_1: 7;

            then ((i + (p .. f)) - ( len f)) <= ( len f) by XREAL_1: 20;

            then

             A50: ((i + (p .. f)) -' ( len f)) <= ( len f) by A49, XREAL_0:def 2;

            

             A51: ((i + (p .. f)) - ( len f)) > 1 by A49;

            then ((i + (p .. f)) -' ( len f)) >= 1 by XREAL_0:def 2;

            then

             A52: ((i + (p .. f)) -' ( len f)) in ( dom f) by A50, FINSEQ_3: 25;

            

             A53: (( Rotate (f,p)) /. i) = (f /. ((i + (p .. f)) -' ( len f))) by A2, A12, A48, FINSEQ_6: 177;

            now

              per cases ;

                suppose

                 A54: j <= ( len (f :- p));

                 A55:

                now

                  assume that

                   A56: ((j -' 1) + (p .. f)) = 1 and

                   A57: ((i + (p .. f)) -' ( len f)) = ( len f);

                  ((i + (p .. f)) - ( len f)) = ( len f) by A49, A57, XREAL_0:def 2;

                  then (i + (p .. f)) = (( len f) + ( len f));

                  then

                   A58: i >= ( len f) by A23, XREAL_1: 8;

                  ((j -' 1) + ((p .. f) - 1)) = 0 by A56;

                  then (j -' 1) = 0 by A3;

                  then (j - 1) = 0 by A18, XREAL_0:def 2;

                  hence contradiction by A8, A16, A12, A58, XXREAL_0: 1;

                end;

                (( Rotate (f,p)) /. j) = (f /. ((j -' 1) + (p .. f))) by A2, A17, A54, FINSEQ_6: 174;

                then (( Rotate (f,p)) . j) = (f /. ((j -' 1) + (p .. f))) by A6, PARTFUN1:def 6;

                then

                 A59: (f /. ((j -' 1) + (p .. f))) = (f /. ((i + (p .. f)) -' ( len f))) by A5, A9, A53, PARTFUN1:def 6;

                

                 A60: ((j -' 1) + (p .. f)) <> ( len f) or ((i + (p .. f)) -' ( len f)) <> 1 by A51, XREAL_0:def 2;

                j in ( dom (f :- p)) by A17, A54, FINSEQ_3: 25;

                then ((j -' 1) + 1) in ( dom (f :- p)) by A17, XREAL_1: 235;

                then

                 A61: ((j -' 1) + (p .. f)) in ( dom f) by A2, FINSEQ_5: 51;

                

                then (f . ((j -' 1) + (p .. f))) = (f /. ((j -' 1) + (p .. f))) by PARTFUN1:def 6

                .= (f . ((i + (p .. f)) -' ( len f))) by A52, A59, PARTFUN1:def 6;

                then ((j -' 1) + (p .. f)) = ((i + (p .. f)) -' ( len f)) by A1, A52, A61, A55, A60;

                then

                 A62: ((j -' 1) + (p .. f)) = ((i + (p .. f)) - ( len f)) by A49, XREAL_0:def 2;

                then

                 A63: (i - ( len f)) = 0 by A13;

                (j - 1) = 0 by A18, A13, A62, XREAL_0:def 2;

                hence thesis by A8, A63, FINSEQ_6: 179;

              end;

                suppose

                 A64: j > ( len (f :- p));

                then (( Rotate (f,p)) /. j) = (f /. ((j + (p .. f)) -' ( len f))) by A2, A14, FINSEQ_6: 177;

                then (( Rotate (f,p)) . j) = (f /. ((j + (p .. f)) -' ( len f))) by A6, PARTFUN1:def 6;

                then

                 A65: (f /. ((j + (p .. f)) -' ( len f))) = (f /. ((i + (p .. f)) -' ( len f))) by A5, A9, A53, PARTFUN1:def 6;

                

                 A66: ((i + (p .. f)) -' ( len f)) <> 1 or ((j + (p .. f)) -' ( len f)) <> ( len f) by A51, XREAL_0:def 2;

                

                 A67: (j - (( len f) - (p .. f))) > 1 by A4, A64, XREAL_1: 20;

                then

                 A68: ((j + (p .. f)) - ( len f)) > 1;

                then

                 A69: ((j + (p .. f)) -' ( len f)) >= 1 by XREAL_0:def 2;

                (j + (p .. f)) <= (( len f) + ( len f)) by A23, A14, XREAL_1: 7;

                then ((j + (p .. f)) - ( len f)) <= ( len f) by XREAL_1: 20;

                then ((j + (p .. f)) -' ( len f)) <= ( len f) by A67, XREAL_0:def 2;

                then

                 A70: ((j + (p .. f)) -' ( len f)) in ( dom f) by A69, FINSEQ_3: 25;

                

                 A71: ((i + (p .. f)) -' ( len f)) <> ( len f) or ((j + (p .. f)) -' ( len f)) <> 1 by A68, XREAL_0:def 2;

                (f . ((i + (p .. f)) -' ( len f))) = (f /. ((i + (p .. f)) -' ( len f))) by A52, PARTFUN1:def 6

                .= (f . ((j + (p .. f)) -' ( len f))) by A65, A70, PARTFUN1:def 6;

                then ((i + (p .. f)) -' ( len f)) = ((j + (p .. f)) -' ( len f)) by A1, A52, A70, A66, A71;

                then ((i + (p .. f)) - ( len f)) = ((j + (p .. f)) -' ( len f)) by A49, XREAL_0:def 2;

                then ((i + (p .. f)) - ( len f)) = ((j + (p .. f)) - ( len f)) by A67, XREAL_0:def 2;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

        suppose not p in ( rng f);

        hence thesis by A1, FINSEQ_6:def 2;

      end;

    end;

    theorem :: JORDAN23:12

    

     Th12: for D be non empty set holds for f be FinSequence of D st f is weakly-one-to-one circular holds for p be Element of D holds ( Rotate (f,p)) is weakly-one-to-one

    proof

      let D be non empty set;

      let f be FinSequence of D;

      assume

       A1: f is weakly-one-to-one circular;

      let p be Element of D;

      per cases ;

        suppose

         A2: p in ( rng f);

        then

         A3: (p .. f) <= ( len f) by FINSEQ_4: 21;

        

         A4: ( len (f :- p)) = ((( len f) - (p .. f)) + 1) by A2, FINSEQ_5: 50;

        let i be Nat;

        1 <= (p .. f) by A2, FINSEQ_4: 21;

        then

         A5: ((i -' 1) + (p .. f)) >= ( 0 + 1) by XREAL_1: 7;

        then

         A6: (((i -' 1) + (p .. f)) + 1) > 1 by NAT_1: 13;

        assume that

         A7: 1 <= i and

         A8: i < ( len ( Rotate (f,p)));

        

         A9: (i + 1) > 1 by A7, NAT_1: 13;

        ((i - 1) + 1) >= 1 by A7;

        then

         A10: (i - 1) >= (1 - 1) by XREAL_1: 20;

        

         A11: (((i + 1) -' 1) + (p .. f)) = (((i + 1) - 1) + (p .. f)) by A7, XREAL_0:def 2

        .= (((i - 1) + (p .. f)) + 1)

        .= (((i -' 1) + (p .. f)) + 1) by A10, XREAL_0:def 2;

        

         A12: (i + 1) <= ( len ( Rotate (f,p))) by A8, NAT_1: 13;

        

         A13: ( len ( Rotate (f,p))) = ( len f) by FINSEQ_6: 179;

        then

         A14: ( len f) > 1 by A7, A8, XXREAL_0: 2;

        then

         A15: ( len f) >= (1 + 1) by NAT_1: 13;

        now

          per cases by XXREAL_0: 1;

            suppose

             A16: i < ( len (f :- p));

            then (i - 1) < (( len f) - (p .. f)) by A4, XREAL_1: 19;

            then ((i - 1) + (p .. f)) < ( len f) by XREAL_1: 20;

            then

             A17: ((i -' 1) + (p .. f)) < ( len f) by A10, XREAL_0:def 2;

            then

             A18: (((i -' 1) + (p .. f)) + 1) <= ( len f) by NAT_1: 13;

            (( Rotate (f,p)) /. i) = (f /. ((i -' 1) + (p .. f))) by A2, A7, A16, FINSEQ_6: 174

            .= (f . ((i -' 1) + (p .. f))) by A5, A17, FINSEQ_4: 15;

            then

             A19: (( Rotate (f,p)) . i) = (f . ((i -' 1) + (p .. f))) by A7, A8, FINSEQ_4: 15;

            (i + 1) <= ( len (f :- p)) by A16, NAT_1: 13;

            

            then (( Rotate (f,p)) /. (i + 1)) = (f /. (((i + 1) -' 1) + (p .. f))) by A2, A9, FINSEQ_6: 174

            .= (f . (((i + 1) -' 1) + (p .. f))) by A6, A11, A18, FINSEQ_4: 15;

            then (( Rotate (f,p)) . (i + 1)) = (f . (((i + 1) -' 1) + (p .. f))) by A9, A12, FINSEQ_4: 15;

            hence thesis by A1, A5, A11, A17, A19;

          end;

            suppose

             A20: i = ( len (f :- p));

            

            then (( Rotate (f,p)) /. i) = (f /. ( len f)) by A2, FINSEQ_6: 176

            .= (f /. 1) by A1, FINSEQ_6:def 1

            .= (f . 1) by A14, FINSEQ_4: 15;

            then

             A21: (( Rotate (f,p)) . i) = (f . 1) by A7, A8, FINSEQ_4: 15;

            

             A22: (((i + 1) + (p .. f)) -' ( len f)) = ((( len f) + (1 + 1)) - ( len f)) by A4, A20, XREAL_0:def 2

            .= 2;

            (i + 1) > ( len (f :- p)) by A20, NAT_1: 13;

            

            then (( Rotate (f,p)) /. (i + 1)) = (f /. (((i + 1) + (p .. f)) -' ( len f))) by A2, A13, A12, FINSEQ_6: 177

            .= (f . (((i + 1) + (p .. f)) -' ( len f))) by A15, A22, FINSEQ_4: 15;

            then (( Rotate (f,p)) . (i + 1)) = (f . (1 + 1)) by A9, A12, A22, FINSEQ_4: 15;

            hence thesis by A1, A14, A21;

          end;

            suppose

             A23: i > ( len (f :- p));

            then

             A24: (i - (( len f) - (p .. f))) > 1 by A4, XREAL_1: 20;

            then ((i + (p .. f)) - ( len f)) > (1 - 1) by XXREAL_0: 2;

            then

             A25: (((i + (p .. f)) - ( len f)) + 1) > 1 by XREAL_1: 19;

            

            then

             A26: (((i + 1) + (p .. f)) -' ( len f)) = (((i + 1) + (p .. f)) - ( len f)) by XREAL_0:def 2

            .= (((i + (p .. f)) - ( len f)) + 1)

            .= (((i + (p .. f)) -' ( len f)) + 1) by A24, XREAL_0:def 2;

            ((i + 1) + (p .. f)) <= (( len f) + ( len f)) by A3, A13, A12, XREAL_1: 7;

            then (((i + 1) + (p .. f)) - ( len f)) <= ( len f) by XREAL_1: 20;

            then

             A27: (((i + 1) + (p .. f)) -' ( len f)) <= ( len f) by A25, XREAL_0:def 2;

            (((i + 1) + (p .. f)) - ( len f)) > 1 by A25;

            then

             A28: (((i + 1) + (p .. f)) -' ( len f)) > 1 by XREAL_0:def 2;

            (i + 1) > ( len (f :- p)) by A23, NAT_1: 13;

            

            then (( Rotate (f,p)) /. (i + 1)) = (f /. (((i + 1) + (p .. f)) -' ( len f))) by A2, A13, A12, FINSEQ_6: 177

            .= (f . (((i + 1) + (p .. f)) -' ( len f))) by A28, A27, FINSEQ_4: 15;

            then

             A29: (( Rotate (f,p)) . (i + 1)) = (f . (((i + 1) + (p .. f)) -' ( len f))) by A9, A12, FINSEQ_4: 15;

            ((i + (p .. f)) - ( len f)) > 1 by A24;

            then

             A30: ((i + (p .. f)) -' ( len f)) > 1 by XREAL_0:def 2;

            (i + (p .. f)) < (( len f) + ( len f)) by A3, A13, A8, XREAL_1: 8;

            then ((i + (p .. f)) - ( len f)) < ( len f) by XREAL_1: 19;

            then

             A31: ((i + (p .. f)) -' ( len f)) < ( len f) by A24, XREAL_0:def 2;

            (( Rotate (f,p)) /. i) = (f /. ((i + (p .. f)) -' ( len f))) by A2, A13, A8, A23, FINSEQ_6: 177

            .= (f . ((i + (p .. f)) -' ( len f))) by A30, A31, FINSEQ_4: 15;

            then (( Rotate (f,p)) . i) = (f . ((i + (p .. f)) -' ( len f))) by A7, A8, FINSEQ_4: 15;

            hence thesis by A1, A30, A31, A29, A26;

          end;

        end;

        hence thesis;

      end;

        suppose not p in ( rng f);

        hence thesis by A1, FINSEQ_6:def 2;

      end;

    end;

    theorem :: JORDAN23:13

    

     Th13: for D be non empty set holds for f be FinSequence of D st f is poorly-one-to-one circular holds for p be Element of D holds ( Rotate (f,p)) is poorly-one-to-one

    proof

      let D be non empty set;

      let f be FinSequence of D;

      assume

       A1: f is poorly-one-to-one circular;

      let p be Element of D;

      

       A2: ( len ( Rotate (f,p))) = ( len f) by FINSEQ_6: 179;

      per cases ;

        suppose

         A3: ( len f) <> 2;

        then f is weakly-one-to-one by A1, Th7;

        then ( Rotate (f,p)) is weakly-one-to-one by A1, Th12;

        hence thesis by A2, A3, Th7;

      end;

        suppose ( len f) = 2;

        hence thesis by A2, Def3;

      end;

    end;

    registration

      let D be non empty set;

      cluster one-to-one circular non empty for FinSequence of D;

      existence

      proof

        set x = the Element of D;

        ( <*x*> /. 1) = ( <*x*> /. ( len <*x*>)) by FINSEQ_1: 39;

        then <*x*> is circular by FINSEQ_6:def 1;

        hence thesis;

      end;

    end

    registration

      let D be non empty set;

      let f be almost-one-to-one FinSequence of D;

      let p be Element of D;

      cluster ( Rotate (f,p)) -> almost-one-to-one;

      coherence by Th11;

    end

    registration

      let D be non empty set;

      let f be circular weakly-one-to-one FinSequence of D;

      let p be Element of D;

      cluster ( Rotate (f,p)) -> weakly-one-to-one;

      coherence by Th12;

    end

    registration

      let D be non empty set;

      let f be circular poorly-one-to-one FinSequence of D;

      let p be Element of D;

      cluster ( Rotate (f,p)) -> poorly-one-to-one;

      coherence by Th13;

    end

    theorem :: JORDAN23:14

    

     Th14: for D be non empty set holds for f be FinSequence of D holds f is almost-one-to-one iff (f /^ 1) is one-to-one & (f | (( len f) -' 1)) is one-to-one

    proof

      let D be non empty set;

      let f be FinSequence of D;

      

       A1: ( len (f /^ 1)) = (( len f) -' 1) by RFINSEQ: 29;

      thus f is almost-one-to-one implies (f /^ 1) is one-to-one & (f | (( len f) -' 1)) is one-to-one

      proof

        assume

         A2: f is almost-one-to-one;

        thus (f /^ 1) is one-to-one

        proof

          let x,y be object;

          assume that

           A3: x in ( dom (f /^ 1)) and

           A4: y in ( dom (f /^ 1)) and

           A5: ((f /^ 1) . x) = ((f /^ 1) . y);

          reconsider i = x, j = y as Nat by A3, A4;

          

           A6: i in ( Seg ( len (f /^ 1))) by A3, FINSEQ_1:def 3;

          then

           A7: 1 <= i by FINSEQ_1: 1;

          

           A8: i <= ( len (f /^ 1)) by A6, FINSEQ_1: 1;

          then (( len f) -' 1) >= 1 by A1, A7, XXREAL_0: 2;

          then

           A9: (( len f) -' 1) = (( len f) - 1) by NAT_D: 39;

          then

           A10: (i + 1) <= ( len f) by A1, A8, XREAL_1: 19;

          then

           A11: ((f /^ 1) . i) = (f . (i + 1)) by A7, FINSEQ_6: 114;

          

           A12: j in ( Seg ( len (f /^ 1))) by A4, FINSEQ_1:def 3;

          then

           A13: 1 <= j by FINSEQ_1: 1;

          j <= ( len (f /^ 1)) by A12, FINSEQ_1: 1;

          then

           A14: (j + 1) <= ( len f) by A1, A9, XREAL_1: 19;

          then

           A15: ((f /^ 1) . j) = (f . (j + 1)) by A13, FINSEQ_6: 114;

          

           A16: (j + 1) > 1 by A13, NAT_1: 13;

          then

           A17: (j + 1) in ( dom f) by A14, FINSEQ_3: 25;

          

           A18: (i + 1) > 1 by A7, NAT_1: 13;

          then (i + 1) in ( dom f) by A10, FINSEQ_3: 25;

          then (i + 1) = (j + 1) by A2, A5, A11, A15, A18, A16, A17;

          hence thesis;

        end;

        

         A19: ( len (f | (( len f) -' 1))) = (( len f) -' 1) by FINSEQ_1: 59, NAT_D: 35;

        thus (f | (( len f) -' 1)) is one-to-one

        proof

          let x,y be object;

          assume that

           A20: x in ( dom (f | (( len f) -' 1))) and

           A21: y in ( dom (f | (( len f) -' 1))) and

           A22: ((f | (( len f) -' 1)) . x) = ((f | (( len f) -' 1)) . y);

          reconsider i = x, j = y as Nat by A20, A21;

          

           A23: i in ( Seg ( len (f | (( len f) -' 1)))) by A20, FINSEQ_1:def 3;

          then

           A24: 1 <= i by FINSEQ_1: 1;

          

           A25: j in ( Seg ( len (f | (( len f) -' 1)))) by A21, FINSEQ_1:def 3;

          then

           A26: j <= ( len (f | (( len f) -' 1))) by FINSEQ_1: 1;

          then

           A27: ((f | (( len f) -' 1)) . j) = (f . j) by A19, FINSEQ_3: 112;

          

           A28: i <= ( len (f | (( len f) -' 1))) by A23, FINSEQ_1: 1;

          then

           A29: ((f | (( len f) -' 1)) . i) = (f . i) by A19, FINSEQ_3: 112;

          (( len f) -' 1) >= 1 by A19, A24, A28, XXREAL_0: 2;

          then

           A30: (( len f) -' 1) = (( len f) - 1) by NAT_D: 39;

          then (j + 1) <= ( len f) by A19, A26, XREAL_1: 19;

          then

           A31: j < ( len f) by NAT_1: 13;

          1 <= j by A25, FINSEQ_1: 1;

          then

           A32: j in ( dom f) by A31, FINSEQ_3: 25;

          (i + 1) <= ( len f) by A19, A28, A30, XREAL_1: 19;

          then

           A33: i < ( len f) by NAT_1: 13;

          then i in ( dom f) by A24, FINSEQ_3: 25;

          hence thesis by A2, A22, A29, A27, A33, A31, A32;

        end;

      end;

      assume that

       A34: (f /^ 1) is one-to-one and

       A35: (f | (( len f) -' 1)) is one-to-one;

      let i,j be Nat;

      assume that

       A36: i in ( dom f) and

       A37: j in ( dom f) and

       A38: i <> 1 or j <> ( len f) and

       A39: i <> ( len f) or j <> 1 and

       A40: (f . i) = (f . j);

      

       A41: ( 0 + 1) <= i by A36, FINSEQ_3: 25;

      then

       A42: (i - 1) >= 0 by XREAL_1: 19;

      

       A43: i <= ( len f) by A36, FINSEQ_3: 25;

      then

       A44: (i - 1) <= (( len f) - 1) by XREAL_1: 9;

      then (i -' 1) <= (( len f) - 1) by A42, XREAL_0:def 2;

      then

       A45: (i -' 1) <= (( len f) -' 1) by XREAL_0:def 2;

      ( len f) = ((( len f) -' 1) + 1) by A41, A43, XREAL_1: 235, XXREAL_0: 2;

      then (( len f) -' 1) <= ( len f) by NAT_1: 13;

      then

       A46: ( len (f | (( len f) -' 1))) = (( len f) -' 1) by FINSEQ_1: 59;

      

       A47: j <= ( len f) by A37, FINSEQ_3: 25;

      then (j - 1) <= (( len f) - 1) by XREAL_1: 9;

      then (j -' 1) <= (( len f) - 1) by A42, A44, XREAL_0:def 2;

      then

       A48: (j -' 1) <= (( len f) -' 1) by XREAL_0:def 2;

      f is non empty by A36;

      then

       A49: f = ( <*(f /. 1)*> ^ (f /^ 1)) by FINSEQ_5: 29;

      

       A50: i = ((i -' 1) + 1) by A41, XREAL_1: 235;

      

       A51: ( 0 + 1) <= j by A37, FINSEQ_3: 25;

      then

       A52: (j - 1) >= 0 by XREAL_1: 19;

      

       A53: j = ((j -' 1) + 1) by A51, XREAL_1: 235;

      per cases ;

        suppose

         A54: i <> 1 & j <> 1;

        then j > ( 0 + 1) by A51, XXREAL_0: 1;

        then (j - 1) > 0 by XREAL_1: 20;

        then (j -' 1) > 0 by XREAL_0:def 2;

        then (j -' 1) >= ( 0 + 1) by NAT_1: 13;

        then

         A55: (j -' 1) in ( dom (f /^ 1)) by A1, A48, FINSEQ_3: 25;

        then

         A56: (f . j) = ((f /^ 1) . (j -' 1)) by A53, A49, FINSEQ_3: 103;

        i > ( 0 + 1) by A41, A54, XXREAL_0: 1;

        then (i - 1) > 0 by XREAL_1: 20;

        then (i -' 1) > 0 by XREAL_0:def 2;

        then (i -' 1) >= ( 0 + 1) by NAT_1: 13;

        then

         A57: (i -' 1) in ( dom (f /^ 1)) by A1, A45, FINSEQ_3: 25;

        then (f . i) = ((f /^ 1) . (i -' 1)) by A50, A49, FINSEQ_3: 103;

        then (i -' 1) = (j -' 1) by A34, A40, A57, A55, A56;

        then (i - 1) = (j -' 1) by A42, XREAL_0:def 2;

        then (i - 1) = (j - 1) by A52, XREAL_0:def 2;

        hence thesis;

      end;

        suppose

         A58: i = 1;

        then j < ( len f) by A38, A47, XXREAL_0: 1;

        then (j + 1) <= ( len f) by NAT_1: 13;

        then j <= (( len f) - 1) by XREAL_1: 19;

        then

         A59: j <= (( len f) -' 1) by XREAL_0:def 2;

        then

         A60: ((f | (( len f) -' 1)) . j) = (f . j) by FINSEQ_3: 112;

        i <= (( len f) -' 1) by A51, A58, A59, XXREAL_0: 2;

        then

         A61: i in ( dom (f | (( len f) -' 1))) by A41, A46, FINSEQ_3: 25;

        

         A62: j in ( dom (f | (( len f) -' 1))) by A51, A46, A59, FINSEQ_3: 25;

        ((f | (( len f) -' 1)) . i) = (f . i) by A51, A58, A59, FINSEQ_3: 112, XXREAL_0: 2;

        hence thesis by A35, A40, A60, A61, A62;

      end;

        suppose

         A63: j = 1;

        then i < ( len f) by A39, A43, XXREAL_0: 1;

        then (i + 1) <= ( len f) by NAT_1: 13;

        then i <= (( len f) - 1) by XREAL_1: 19;

        then

         A64: i <= (( len f) -' 1) by XREAL_0:def 2;

        then

         A65: ((f | (( len f) -' 1)) . i) = (f . i) by FINSEQ_3: 112;

        j <= (( len f) -' 1) by A41, A63, A64, XXREAL_0: 2;

        then

         A66: j in ( dom (f | (( len f) -' 1))) by A51, A46, FINSEQ_3: 25;

        

         A67: i in ( dom (f | (( len f) -' 1))) by A41, A46, A64, FINSEQ_3: 25;

        ((f | (( len f) -' 1)) . j) = (f . j) by A41, A63, A64, FINSEQ_3: 112, XXREAL_0: 2;

        hence thesis by A35, A40, A65, A67, A66;

      end;

    end;

    registration

      let C be compact non vertical non horizontal Subset of ( TOP-REAL 2);

      let n be Nat;

      cluster ( Cage (C,n)) -> almost-one-to-one;

      coherence

      proof

        ( len ( Cage (C,n))) > ( 0 + 1) by GOBOARD7: 34, XXREAL_0: 2;

        then (( len ( Cage (C,n))) - 1) > 0 by XREAL_1: 20;

        then

         A1: (( len ( Cage (C,n))) -' 1) = (( len ( Cage (C,n))) - 1) by XREAL_0:def 2;

        

         A2: ( len ( Cage (C,n))) > 4 by GOBOARD7: 34;

        ( len ( Cage (C,n))) < (( len ( Cage (C,n))) + 1) by NAT_1: 13;

        then (( len ( Cage (C,n))) -' 1) < ( len ( Cage (C,n))) by A1, XREAL_1: 19;

        then

         A3: (( Cage (C,n)) | (( len ( Cage (C,n))) -' 1)) is one-to-one by A2, TOPREAL8: 22;

        (( Cage (C,n)) /^ 1) is one-to-one;

        hence thesis by A3, Th14;

      end;

    end

    registration

      let C be compact non vertical non horizontal Subset of ( TOP-REAL 2);

      let n be Nat;

      cluster ( Cage (C,n)) -> weakly-one-to-one;

      coherence

      proof

        ( len ( Cage (C,n))) > 2 by GOBOARD7: 34, XXREAL_0: 2;

        hence thesis by Th7;

      end;

    end

    theorem :: JORDAN23:15

    

     Th15: for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) & f is weakly-one-to-one holds ( B_Cut (f,p,p)) = <*p*>

    proof

      let f be FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2);

      assume that

       A1: p in ( L~ f) and

       A2: f is weakly-one-to-one;

      

       A3: 1 <= ( Index (p,f)) by A1, JORDAN3: 8;

      (( L_Cut (f,p)) . 1) = p by A1, JORDAN3: 23;

      then

       A4: ( R_Cut (( L_Cut (f,p)),p)) = <*p*> by JORDAN3:def 4;

      

       A5: ( Index (p,f)) < ( len f) by A1, JORDAN3: 8;

      then

       A6: (( Index (p,f)) + 1) <= ( len f) by NAT_1: 13;

      then

       A7: (( Index (p,f)) + 1) in ( dom f) by A3, SEQ_4: 134;

      (f . ( Index (p,f))) <> (f . (( Index (p,f)) + 1)) by A2, A5, A3;

      then

       A8: (f . ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A7, PARTFUN1:def 6;

      ( Index (p,f)) in ( dom f) by A3, A6, SEQ_4: 134;

      then

       A9: (f /. ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A8, PARTFUN1:def 6;

      p in ( LSeg (f,( Index (p,f)))) by A1, JORDAN3: 9;

      then p in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A3, A6, TOPREAL1:def 3;

      then LE (p,p,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A9, JORDAN5B: 9;

      hence thesis by A4, JORDAN3:def 7;

    end;

    theorem :: JORDAN23:16

    

     Th16: for f be FinSequence st f is one-to-one holds f is weakly-one-to-one

    proof

      let f be FinSequence;

      assume

       A1: f is one-to-one;

      for i be Nat st 1 <= i & i < ( len f) holds (f . i) <> (f . (i + 1))

      proof

        let i be Nat;

        assume that

         A2: 1 <= i and

         A3: i < ( len f);

        

         A4: (i + 1) in ( dom f) by A2, A3, MSUALG_8: 1;

        

         A5: i <> (i + 1);

        i in ( dom f) by A2, A3, MSUALG_8: 1;

        hence thesis by A1, A4, A5;

      end;

      hence thesis;

    end;

    registration

      cluster one-to-one -> weakly-one-to-one for FinSequence;

      coherence by Th16;

    end

    theorem :: JORDAN23:17

    

     Th17: for f be FinSequence of ( TOP-REAL 2) st f is weakly-one-to-one holds for p,q be Point of ( TOP-REAL 2) st p in ( L~ f) & q in ( L~ f) holds ( B_Cut (f,p,q)) = ( Rev ( B_Cut (f,q,p)))

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is weakly-one-to-one;

      let p,q be Point of ( TOP-REAL 2) such that

       A2: p in ( L~ f) and

       A3: q in ( L~ f);

      per cases ;

        suppose

         A4: p = q;

        then ( B_Cut (f,p,q)) = <*p*> by A1, A2, Th15;

        hence thesis by A4, FINSEQ_5: 60;

      end;

        suppose that

         A5: p <> q and

         A6: ( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

         not (( Index (q,f)) = ( Index (p,f)) & LE (q,p,(f /. ( Index (q,f))),(f /. (( Index (q,f)) + 1)))) by A5, A6, JORDAN3: 27;

        then

         A7: ( Rev ( B_Cut (f,q,p))) = ( Rev ( Rev ( R_Cut (( L_Cut (f,p)),q)))) by A6, JORDAN3:def 7;

        ( B_Cut (f,p,q)) = ( R_Cut (( L_Cut (f,p)),q)) by A2, A3, A6, JORDAN3:def 7;

        hence thesis by A7;

      end;

        suppose that p <> q and

         A8: not (( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

        

         A9: ( Index (q,f)) < ( Index (p,f)) or ( Index (p,f)) = ( Index (q,f)) & not LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A8, XXREAL_0: 1;

         A10:

        now

          assume that

           A11: ( Index (p,f)) = ( Index (q,f)) and

           A12: not LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

          

           A13: 1 <= ( Index (p,f)) by A2, JORDAN3: 8;

          

           A14: ( Index (p,f)) < ( len f) by A2, JORDAN3: 8;

          then

           A15: (( Index (p,f)) + 1) <= ( len f) by NAT_1: 13;

          then

           A16: ( LSeg (f,( Index (p,f)))) = ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A13, TOPREAL1:def 3;

          then

           A17: p in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A2, JORDAN3: 9;

          1 <= (( Index (p,f)) + 1) by NAT_1: 11;

          then

           A18: (( Index (p,f)) + 1) in ( dom f) by A15, FINSEQ_3: 25;

          (f . ( Index (p,f))) <> (f . (( Index (p,f)) + 1)) by A1, A13, A14;

          then

           A19: (f . ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A18, PARTFUN1:def 6;

          ( Index (p,f)) in ( dom f) by A13, A14, FINSEQ_3: 25;

          then

           A20: (f /. ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A19, PARTFUN1:def 6;

          q in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A3, A11, A16, JORDAN3: 9;

          then LT (q,p,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A12, A17, A20, JORDAN3: 28;

          hence LE (q,p,(f /. ( Index (q,f))),(f /. (( Index (q,f)) + 1))) by A11, JORDAN3:def 6;

        end;

        ( B_Cut (f,p,q)) = ( Rev ( R_Cut (( L_Cut (f,q)),p))) by A8, JORDAN3:def 7;

        hence thesis by A2, A3, A9, A10, JORDAN3:def 7;

      end;

    end;

    theorem :: JORDAN23:18

    

     Th18: for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) holds for i1 be Nat st f is poorly-one-to-one unfolded s.n.c. & 1 < i1 & i1 <= ( len f) & p = (f . i1) holds (( Index (p,f)) + 1) = i1

    proof

      let f be FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2), i1 be Nat;

      assume

       A1: f is poorly-one-to-one unfolded s.n.c.;

      assume that

       A2: 1 < i1 and

       A3: i1 <= ( len f);

      consider j be Nat such that

       A4: i1 = (j + 1) by A2, NAT_1: 6;

      reconsider j as Nat;

      

       A5: (1 + 0 ) <= j by A2, A4, NAT_1: 13;

      assume

       A6: p = (f . i1);

      assume

       A7: (( Index (p,f)) + 1) <> i1;

      

       A8: j in NAT by ORDINAL1:def 12;

      i1 in ( dom f) by A2, A3, FINSEQ_3: 25;

      then p = (f /. i1) by A6, PARTFUN1:def 6;

      then

       A9: p in ( LSeg (f,j)) by A3, A4, A5, TOPREAL1: 21;

      then ( Index (p,f)) <= j by A8, JORDAN3: 7;

      then ( Index (p,f)) < j by A4, A7, XXREAL_0: 1;

      then

       A10: (( Index (p,f)) + 1) <= j by NAT_1: 13;

      

       A11: ( LSeg (f,j)) c= ( L~ f) by TOPREAL3: 19;

      then

       A12: p in ( LSeg (f,( Index (p,f)))) by A9, JORDAN3: 9;

      per cases by A10, XXREAL_0: 1;

        suppose

         A13: (( Index (p,f)) + 1) = j;

        

         A14: 1 <= ( Index (p,f)) by A9, A11, JORDAN3: 8;

        then (( Index (p,f)) + 2) >= (1 + 2) by XREAL_1: 7;

        then ( len f) >= (2 + 1) by A3, A4, A13, XXREAL_0: 2;

        then

         A15: ( len f) > 2 by NAT_1: 13;

        (( Index (p,f)) + (1 + 1)) <= ( len f) by A3, A4, A13;

        then (( LSeg (f,( Index (p,f)))) /\ ( LSeg (f,j))) = {(f /. j)} by A1, A13, A14, TOPREAL1:def 6;

        then

         A16: p in {(f /. j)} by A9, A12, XBOOLE_0:def 4;

        

         A17: j < ( len f) by A3, A4, NAT_1: 13;

        then j in ( dom f) by A5, FINSEQ_3: 25;

        

        then (f . j) = (f /. j) by PARTFUN1:def 6

        .= (f . i1) by A6, A16, TARSKI:def 1;

        hence contradiction by A1, A4, A5, A17, A15, Def3;

      end;

        suppose

         A18: (( Index (p,f)) + 1) < j;

        p in (( LSeg (f,( Index (p,f)))) /\ ( LSeg (f,j))) by A9, A12, XBOOLE_0:def 4;

        then ( LSeg (f,( Index (p,f)))) meets ( LSeg (f,j));

        hence contradiction by A1, A18, TOPREAL1:def 7;

      end;

    end;

    theorem :: JORDAN23:19

    

     Th19: for f be FinSequence of ( TOP-REAL 2) st f is weakly-one-to-one holds for p,q be Point of ( TOP-REAL 2) st p in ( L~ f) & q in ( L~ f) holds (( B_Cut (f,p,q)) /. 1) = p

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is weakly-one-to-one;

      let p,q be Point of ( TOP-REAL 2);

      assume that

       A2: p in ( L~ f) and

       A3: q in ( L~ f);

      

       A4: ( Index (p,f)) < ( len f) by A2, JORDAN3: 8;

      

       A5: 1 <= ( Index (p,f)) by A2, JORDAN3: 8;

      then

       A6: ( Index (p,f)) in ( dom f) by A4, FINSEQ_3: 25;

      

       A7: 1 <= ( len ( L_Cut (f,p))) by A2, Th1;

      per cases ;

        suppose

         A8: p <> q;

        now

          per cases ;

            suppose

             A9: p in ( L~ f) & q in ( L~ f) & ( Index (p,f)) < ( Index (q,f));

            then q in ( L~ ( L_Cut (f,p))) by JORDAN3: 29;

            

            then (( R_Cut (( L_Cut (f,p)),q)) /. 1) = (( L_Cut (f,p)) /. 1) by SPRECT_3: 22

            .= (( L_Cut (f,p)) . 1) by A7, FINSEQ_4: 15

            .= p by A9, JORDAN3: 23;

            hence thesis by A9, JORDAN3:def 7;

          end;

            suppose

             A10: ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

            then q in ( L~ ( L_Cut (f,p))) by A2, A3, A8, JORDAN3: 31;

            

            then (( R_Cut (( L_Cut (f,p)),q)) /. 1) = (( L_Cut (f,p)) /. 1) by SPRECT_3: 22

            .= (( L_Cut (f,p)) . 1) by A7, FINSEQ_4: 15

            .= p by A2, JORDAN3: 23;

            hence thesis by A10, JORDAN3:def 7;

          end;

            suppose

             A11: not (p in ( L~ f) & q in ( L~ f) & ( Index (p,f)) < ( Index (q,f))) & not (( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

            then

             A12: ( B_Cut (f,p,q)) = ( Rev ( R_Cut (( L_Cut (f,q)),p))) by JORDAN3:def 7;

            now

              per cases by A2, A3, A11, XXREAL_0: 1;

                suppose ( Index (p,f)) > ( Index (q,f));

                then

                 A13: p in ( L~ ( L_Cut (f,q))) by A2, A3, JORDAN3: 29;

                ( R_Cut (( L_Cut (f,q)),p)) <> {} by JORDAN1J: 44;

                

                hence (( B_Cut (f,p,q)) /. 1) = (( R_Cut (( L_Cut (f,q)),p)) /. ( len ( R_Cut (( L_Cut (f,q)),p)))) by A12, FINSEQ_5: 65

                .= p by A13, JORDAN1J: 45;

              end;

                suppose

                 A14: ( Index (p,f)) = ( Index (q,f));

                

                 A15: (( Index (p,f)) + 1) >= 1 by NAT_1: 11;

                (( Index (p,f)) + 1) <= ( len f) by A4, NAT_1: 13;

                then

                 A16: (( Index (p,f)) + 1) in ( dom f) by A15, FINSEQ_3: 25;

                set Ls = ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

                

                 A17: q in Ls by A3, A14, JORDAN5B: 29;

                

                 A18: p in Ls by A2, JORDAN5B: 29;

                (f . ( Index (p,f))) <> (f . (( Index (p,f)) + 1)) by A1, A5, A4;

                then (f . ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A16, PARTFUN1:def 6;

                then

                 A19: (f /. ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A6, PARTFUN1:def 6;

                then

                 A20: Ls is_an_arc_of ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by TOPREAL1: 9;

                 not LE (p,q,Ls,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A11, A14, A19, JORDAN5C: 17;

                then LE (q,p,Ls,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A8, A20, A18, A17, JORDAN5C: 14;

                then

                 A21: p in ( L~ ( L_Cut (f,q))) by A2, A3, A8, A14, A19, JORDAN3: 31, JORDAN5C: 17;

                ( R_Cut (( L_Cut (f,q)),p)) <> {} by JORDAN1J: 44;

                

                hence (( B_Cut (f,p,q)) /. 1) = (( R_Cut (( L_Cut (f,q)),p)) /. ( len ( R_Cut (( L_Cut (f,q)),p)))) by A12, FINSEQ_5: 65

                .= p by A21, JORDAN1J: 45;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

        suppose p = q;

        then ( B_Cut (f,p,q)) = <*p*> by A1, A2, Th15;

        hence thesis by FINSEQ_4: 16;

      end;

    end;

    theorem :: JORDAN23:20

    

     Th20: for f be FinSequence of ( TOP-REAL 2) st f is weakly-one-to-one holds for p,q be Point of ( TOP-REAL 2) st p in ( L~ f) & q in ( L~ f) holds (( B_Cut (f,p,q)) /. ( len ( B_Cut (f,p,q)))) = q

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is weakly-one-to-one;

      let p,q be Point of ( TOP-REAL 2) such that

       A2: p in ( L~ f) and

       A3: q in ( L~ f);

      

       A4: ( B_Cut (f,q,p)) <> {} by Th3;

      ( B_Cut (f,p,q)) = ( Rev ( B_Cut (f,q,p))) by A1, A2, A3, Th17;

      

      hence (( B_Cut (f,p,q)) /. ( len ( B_Cut (f,p,q)))) = (( Rev ( B_Cut (f,q,p))) /. ( len ( B_Cut (f,q,p)))) by FINSEQ_5:def 3

      .= (( B_Cut (f,q,p)) /. 1) by A4, FINSEQ_5: 65

      .= q by A1, A2, A3, Th19;

    end;

    theorem :: JORDAN23:21

    for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) holds ( L~ ( L_Cut (f,p))) c= ( L~ f)

    proof

      let f be FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2) such that

       A1: p in ( L~ f);

      ( Index (p,f)) < ( len f) by A1, JORDAN3: 8;

      then

       A2: (( Index (p,f)) + 1) <= ( len f) by NAT_1: 13;

      ( len f) <> 0 by A1, TOPREAL1: 22;

      then ( len f) > 0 by NAT_1: 3;

      then

       A3: ( len f) >= ( 0 + 1) by NAT_1: 13;

      then

       A4: ( len f) in ( dom f) by FINSEQ_3: 25;

      

       A5: 1 <= ( Index (p,f)) by A1, JORDAN3: 8;

      then

       A6: 1 < (( Index (p,f)) + 1) by NAT_1: 13;

      then

       A7: (( Index (p,f)) + 1) in ( dom f) by A2, FINSEQ_3: 25;

      per cases ;

        suppose p = (f . (( Index (p,f)) + 1));

        then ( L_Cut (f,p)) = ( mid (f,(( Index (p,f)) + 1),( len f))) by JORDAN3:def 3;

        hence thesis by A3, A6, A2, JORDAN4: 35;

      end;

        suppose p <> (f . (( Index (p,f)) + 1));

        then

         A8: ( L_Cut (f,p)) = ( <*p*> ^ ( mid (f,(( Index (p,f)) + 1),( len f)))) by JORDAN3:def 3;

        

         A9: (f /. (( Index (p,f)) + 1)) in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by RLTOPSP1: 68;

        p in ( LSeg (f,( Index (p,f)))) by A1, JORDAN3: 9;

        then

         A10: p in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A5, A2, TOPREAL1:def 3;

        

         A11: ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) c= ( L~ f) by A1, A2, JORDAN3: 8, SPPOL_2: 16;

        (( mid (f,(( Index (p,f)) + 1),( len f))) /. 1) = (f /. (( Index (p,f)) + 1)) by A4, A7, SPRECT_2: 8;

        then ( LSeg (p,(( mid (f,(( Index (p,f)) + 1),( len f))) /. 1))) c= ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A10, A9, TOPREAL1: 6;

        then

         A12: ( LSeg (p,(( mid (f,(( Index (p,f)) + 1),( len f))) /. 1))) c= ( L~ f) by A11;

        ( len ( mid (f,(( Index (p,f)) + 1),( len f)))) >= ( 0 + 1) by A4, A7, SPRECT_2: 5;

        then ( mid (f,(( Index (p,f)) + 1),( len f))) <> {} ;

        then

         A13: ( L~ ( <*p*> ^ ( mid (f,(( Index (p,f)) + 1),( len f))))) = (( LSeg (p,(( mid (f,(( Index (p,f)) + 1),( len f))) /. 1))) \/ ( L~ ( mid (f,(( Index (p,f)) + 1),( len f))))) by SPPOL_2: 20;

        ( L~ ( mid (f,(( Index (p,f)) + 1),( len f)))) c= ( L~ f) by A3, A6, A2, JORDAN4: 35;

        hence thesis by A8, A13, A12, XBOOLE_1: 8;

      end;

    end;

    theorem :: JORDAN23:22

    for f be FinSequence of ( TOP-REAL 2) holds for p,q be Point of ( TOP-REAL 2) st p in ( L~ f) & q in ( L~ f) & f is weakly-one-to-one holds ( L~ ( B_Cut (f,p,q))) c= ( L~ f)

    proof

      let f be FinSequence of ( TOP-REAL 2);

      let p,q be Point of ( TOP-REAL 2) such that

       A1: p in ( L~ f) and

       A2: q in ( L~ f) and

       A3: f is weakly-one-to-one;

      per cases ;

        suppose p = q;

        then ( B_Cut (f,p,q)) = <*p*> by A1, A3, Th15;

        then ( len ( B_Cut (f,p,q))) = 1 by FINSEQ_1: 39;

        then ( L~ ( B_Cut (f,p,q))) = {} by TOPREAL1: 22;

        hence thesis;

      end;

        suppose p <> q & (( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

        hence thesis by A1, A2, JORDAN5B: 33;

      end;

        suppose that

         A4: p <> q and

         A5: not (( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

         A6:

        now

          assume that

           A7: ( Index (p,f)) = ( Index (q,f)) and

           A8: not LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

          

           A9: ( Index (p,f)) < ( len f) by A1, JORDAN3: 8;

          

           A10: 1 <= ( Index (p,f)) by A1, JORDAN3: 8;

          then

           A11: ( Index (p,f)) in ( dom f) by A9, FINSEQ_3: 25;

          

           A12: (( Index (p,f)) + 1) <= ( len f) by A9, NAT_1: 13;

          then

           A13: ( LSeg (f,( Index (p,f)))) = ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A10, TOPREAL1:def 3;

          then

           A14: p in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A1, JORDAN3: 9;

          (f . ( Index (p,f))) <> (f . (( Index (p,f)) + 1)) by A3, A10, A9;

          then

           A15: (f /. ( Index (p,f))) <> (f . (( Index (p,f)) + 1)) by A11, PARTFUN1:def 6;

          1 <= (( Index (p,f)) + 1) by NAT_1: 11;

          then (( Index (p,f)) + 1) in ( dom f) by A12, FINSEQ_3: 25;

          then

           A16: (f /. ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A15, PARTFUN1:def 6;

          q in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A2, A7, A13, JORDAN3: 9;

          then LT (q,p,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A8, A14, A16, JORDAN3: 28;

          hence LE (q,p,(f /. ( Index (q,f))),(f /. (( Index (q,f)) + 1))) by A7, JORDAN3:def 6;

        end;

        

         A17: ( Index (q,f)) < ( Index (p,f)) or ( Index (p,f)) = ( Index (q,f)) & not LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A5, XXREAL_0: 1;

        then

         A18: ( L~ ( B_Cut (f,q,p))) c= ( L~ f) by A1, A2, A4, A6, JORDAN5B: 33;

        ( B_Cut (f,p,q)) = ( Rev ( R_Cut (( L_Cut (f,q)),p))) by A5, JORDAN3:def 7;

        then ( Rev ( B_Cut (f,q,p))) = ( B_Cut (f,p,q)) by A1, A2, A17, A6, JORDAN3:def 7;

        hence thesis by A18, SPPOL_2: 22;

      end;

    end;

    theorem :: JORDAN23:23

    

     Th23: for f,g be FinSequence holds ( dom f) c= ( dom (f ^' g))

    proof

      let f,g be FinSequence;

      ( len f) <= ( len (f ^' g)) by TOPREAL8: 7;

      hence thesis by FINSEQ_3: 30;

    end;

    theorem :: JORDAN23:24

    for f be non empty FinSequence holds for g be FinSequence holds ( dom g) c= ( dom (f ^' g))

    proof

      let f be non empty FinSequence;

      let g be FinSequence;

      ( len g) <= ( len (f ^' g)) by TOPREAL8: 9;

      hence thesis by FINSEQ_3: 30;

    end;

    theorem :: JORDAN23:25

    

     Th25: for f,g be FinSequence st (f ^' g) is constant holds f is constant

    proof

      let f,g be FinSequence;

      assume (f ^' g) is constant;

      then

      reconsider h = (f ^' g) as constant FinSequence;

      ( rng f) c= ( rng h) by TOPREAL8: 10;

      hence thesis;

    end;

    theorem :: JORDAN23:26

    for f,g be FinSequence st (f ^' g) is constant & (f . ( len f)) = (g . 1) & f <> {} holds g is constant

    proof

      let f,g be FinSequence;

      assume that

       A1: (f ^' g) is constant and

       A2: (f . ( len f)) = (g . 1) and

       A3: f <> {} ;

      reconsider h = (f ^' g) as constant FinSequence by A1;

      per cases ;

        suppose g <> {} ;

        then ( rng h) = (( rng f) \/ ( rng g)) by A2, A3, FINSEQ_6: 144;

        then ( rng g) c= ( rng h) by XBOOLE_1: 7;

        hence thesis;

      end;

        suppose g = {} ;

        hence thesis;

      end;

    end;

    theorem :: JORDAN23:27

    

     Th27: for f be special FinSequence of ( TOP-REAL 2) holds for i,j be Nat holds ( mid (f,i,j)) is special

    proof

      let f be special FinSequence of ( TOP-REAL 2);

      let i,j be Nat;

      per cases ;

        suppose i <= j;

        then ( mid (f,i,j)) = ((f /^ (i -' 1)) | ((j -' i) + 1)) by FINSEQ_6:def 3;

        hence thesis;

      end;

        suppose j < i;

        then ( mid (f,j,i)) = ((f /^ (j -' 1)) | ((i -' j) + 1)) by FINSEQ_6:def 3;

        then ( Rev ( mid (f,i,j))) is special by JORDAN4: 18;

        then ( Rev ( Rev ( mid (f,i,j)))) is special by SPPOL_2: 40;

        hence thesis;

      end;

    end;

    theorem :: JORDAN23:28

    

     Th28: for f be unfolded FinSequence of ( TOP-REAL 2) holds for i,j be Nat holds ( mid (f,i,j)) is unfolded

    proof

      let f be unfolded FinSequence of ( TOP-REAL 2);

      let i,j be Nat;

      per cases ;

        suppose i <= j;

        then ( mid (f,i,j)) = ((f /^ (i -' 1)) | ((j -' i) + 1)) by FINSEQ_6:def 3;

        hence thesis;

      end;

        suppose j < i;

        then ( mid (f,j,i)) = ((f /^ (j -' 1)) | ((i -' j) + 1)) by FINSEQ_6:def 3;

        then ( Rev ( mid (f,i,j))) is unfolded by JORDAN4: 18;

        then ( Rev ( Rev ( mid (f,i,j)))) is unfolded by SPPOL_2: 28;

        hence thesis;

      end;

    end;

    theorem :: JORDAN23:29

    

     Th29: for f be FinSequence of ( TOP-REAL 2) st f is special holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) holds ( L_Cut (f,p)) is special

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is special;

      let p be Point of ( TOP-REAL 2);

      

       A2: ( mid (f,(( Index (p,f)) + 1),( len f))) is special by A1, Th27;

      

       A3: ( <*p*> /. 1) = p by FINSEQ_4: 16;

      assume

       A4: p in ( L~ f);

      then ( Index (p,f)) < ( len f) by JORDAN3: 8;

      then

       A5: (( Index (p,f)) + 1) <= ( len f) by NAT_1: 13;

      1 <= ( Index (p,f)) by A4, JORDAN3: 8;

      then

       A6: ( LSeg (f,( Index (p,f)))) = ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A5, TOPREAL1:def 3;

       A7:

      now

        per cases by A1, SPPOL_1: 19;

          case ( LSeg (f,( Index (p,f)))) is vertical;

          hence (p `1 ) = ((f /. (( Index (p,f)) + 1)) `1 ) by A4, A6, JORDAN5B: 29, SPPOL_1: 41;

        end;

          case ( LSeg (f,( Index (p,f)))) is horizontal;

          hence (p `2 ) = ((f /. (( Index (p,f)) + 1)) `2 ) by A4, A6, JORDAN5B: 29, SPPOL_1: 40;

        end;

      end;

      

       A8: ( len <*p*>) = 1 by FINSEQ_1: 39;

      ( len f) <> 0 by A4, TOPREAL1: 22;

      then ( len f) > 0 by NAT_1: 3;

      then ( len f) >= ( 0 + 1) by NAT_1: 13;

      then

       A9: ( len f) in ( dom f) by FINSEQ_3: 25;

      (( Index (p,f)) + 1) >= 1 by NAT_1: 11;

      then (( Index (p,f)) + 1) in ( dom f) by A5, FINSEQ_3: 25;

      then

       A10: (( mid (f,(( Index (p,f)) + 1),( len f))) /. 1) = (f /. (( Index (p,f)) + 1)) by A9, SPRECT_2: 8;

      per cases ;

        suppose p <> (f . (( Index (p,f)) + 1));

        then ( L_Cut (f,p)) = ( <*p*> ^ ( mid (f,(( Index (p,f)) + 1),( len f)))) by JORDAN3:def 3;

        hence thesis by A2, A8, A3, A10, A7, GOBOARD2: 8;

      end;

        suppose p = (f . (( Index (p,f)) + 1));

        hence thesis by A2, JORDAN3:def 3;

      end;

    end;

    theorem :: JORDAN23:30

    

     Th30: for f be FinSequence of ( TOP-REAL 2) st f is special holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) holds ( R_Cut (f,p)) is special

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is special;

      let p be Point of ( TOP-REAL 2);

      

       A2: ( mid (f,1,( Index (p,f)))) is special by A1, Th27;

      assume

       A3: p in ( L~ f);

      then

       A4: ( Index (p,f)) < ( len f) by JORDAN3: 8;

      ( len f) <> 0 by A3, TOPREAL1: 22;

      then ( len f) > 0 by NAT_1: 3;

      then ( len f) >= ( 0 + 1) by NAT_1: 13;

      then

       A5: 1 in ( dom f) by FINSEQ_3: 25;

      

       A6: 1 <= ( Index (p,f)) by A3, JORDAN3: 8;

      then ( Index (p,f)) in ( dom f) by A4, FINSEQ_3: 25;

      then

       A7: (( mid (f,1,( Index (p,f)))) /. ( len ( mid (f,1,( Index (p,f)))))) = (f /. ( Index (p,f))) by A5, SPRECT_2: 9;

      (( Index (p,f)) + 1) <= ( len f) by A4, NAT_1: 13;

      then

       A8: ( LSeg (f,( Index (p,f)))) = ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A6, TOPREAL1:def 3;

       A9:

      now

        per cases by A1, SPPOL_1: 19;

          case ( LSeg (f,( Index (p,f)))) is vertical;

          hence (p `1 ) = ((f /. ( Index (p,f))) `1 ) by A3, A8, JORDAN5B: 29, SPPOL_1: 41;

        end;

          case ( LSeg (f,( Index (p,f)))) is horizontal;

          hence (p `2 ) = ((f /. ( Index (p,f))) `2 ) by A3, A8, JORDAN5B: 29, SPPOL_1: 40;

        end;

      end;

      

       A10: ( <*p*> /. 1) = p by FINSEQ_4: 16;

      

       A11: <*p*> is special;

      per cases ;

        suppose p <> (f . 1);

        then ( R_Cut (f,p)) = (( mid (f,1,( Index (p,f)))) ^ <*p*>) by JORDAN3:def 4;

        hence thesis by A2, A10, A7, A9, GOBOARD2: 8;

      end;

        suppose p = (f . 1);

        hence thesis by A11, JORDAN3:def 4;

      end;

    end;

    theorem :: JORDAN23:31

    for f be FinSequence of ( TOP-REAL 2) st f is special weakly-one-to-one holds for p,q be Point of ( TOP-REAL 2) st p in ( L~ f) & q in ( L~ f) holds ( B_Cut (f,p,q)) is special

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is special weakly-one-to-one;

      let p,q be Point of ( TOP-REAL 2);

      assume that

       A2: p in ( L~ f) and

       A3: q in ( L~ f);

      

       A4: ( Index (p,f)) < ( len f) by A2, JORDAN3: 8;

      

       A5: 1 <= ( Index (p,f)) by A2, JORDAN3: 8;

      then

       A6: ( Index (p,f)) in ( dom f) by A4, FINSEQ_3: 25;

      per cases ;

        suppose

         A7: p <> q;

        now

          per cases ;

            suppose

             A8: p in ( L~ f) & q in ( L~ f) & ( Index (p,f)) < ( Index (q,f));

            then

             A9: q in ( L~ ( L_Cut (f,p))) by JORDAN3: 29;

            ( L_Cut (f,p)) is special by A1, A2, Th29;

            then ( R_Cut (( L_Cut (f,p)),q)) is special by A9, Th30;

            hence thesis by A8, JORDAN3:def 7;

          end;

            suppose

             A10: ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

            

             A11: ( L_Cut (f,p)) is special by A1, A2, Th29;

            q in ( L~ ( L_Cut (f,p))) by A2, A3, A7, A10, JORDAN3: 31;

            then ( R_Cut (( L_Cut (f,p)),q)) is special by A11, Th30;

            hence thesis by A10, JORDAN3:def 7;

          end;

            suppose

             A12: not (p in ( L~ f) & q in ( L~ f) & ( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

             A13:

            now

              per cases by A2, A3, A12, XXREAL_0: 1;

                suppose ( Index (q,f)) < ( Index (p,f));

                hence p in ( L~ ( L_Cut (f,q))) by A2, A3, JORDAN3: 29;

              end;

                suppose

                 A14: ( Index (q,f)) = ( Index (p,f));

                

                 A15: (( Index (p,f)) + 1) >= 1 by NAT_1: 11;

                (( Index (p,f)) + 1) <= ( len f) by A4, NAT_1: 13;

                then

                 A16: (( Index (p,f)) + 1) in ( dom f) by A15, FINSEQ_3: 25;

                set Ls = ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

                

                 A17: q in Ls by A3, A14, JORDAN5B: 29;

                

                 A18: p in Ls by A2, JORDAN5B: 29;

                (f . ( Index (p,f))) <> (f . (( Index (p,f)) + 1)) by A1, A5, A4;

                then (f . ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A16, PARTFUN1:def 6;

                then

                 A19: (f /. ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A6, PARTFUN1:def 6;

                then

                 A20: Ls is_an_arc_of ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by TOPREAL1: 9;

                 not LE (p,q,Ls,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A12, A14, A19, JORDAN5C: 17;

                then LE (q,p,Ls,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A7, A20, A18, A17, JORDAN5C: 14;

                hence p in ( L~ ( L_Cut (f,q))) by A2, A3, A7, A14, A19, JORDAN3: 31, JORDAN5C: 17;

              end;

            end;

            

             A21: ( B_Cut (f,p,q)) = ( Rev ( R_Cut (( L_Cut (f,q)),p))) by A12, JORDAN3:def 7;

            ( L_Cut (f,q)) is special by A1, A3, Th29;

            then ( R_Cut (( L_Cut (f,q)),p)) is special by A13, Th30;

            hence thesis by A21, SPPOL_2: 40;

          end;

        end;

        hence thesis;

      end;

        suppose p = q;

        then ( B_Cut (f,p,q)) = <*p*> by A1, A2, Th15;

        hence thesis;

      end;

    end;

    theorem :: JORDAN23:32

    

     Th32: for f be FinSequence of ( TOP-REAL 2) st f is unfolded holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) holds ( L_Cut (f,p)) is unfolded

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is unfolded;

      let p be Point of ( TOP-REAL 2);

      

       A2: ( mid (f,(( Index (p,f)) + 1),( len f))) is unfolded by A1, Th28;

      assume

       A3: p in ( L~ f);

      then

       A4: p in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by JORDAN5B: 29;

      ( Index (p,f)) < ( len f) by A3, JORDAN3: 8;

      then

       A5: ((( Index (p,f)) + 1) + 0 ) <= ( len f) by NAT_1: 13;

      ( len f) <> 0 by A3, TOPREAL1: 22;

      then ( len f) > 0 by NAT_1: 3;

      then

       A6: ( len f) >= ( 0 + 1) by NAT_1: 13;

      then

       A7: ( len f) in ( dom f) by FINSEQ_3: 25;

      

       A8: 1 <= ( Index (p,f)) by A3, JORDAN3: 8;

      then

       A9: ( LSeg (f,( Index (p,f)))) = ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A5, TOPREAL1:def 3;

      

       A10: 1 < (( Index (p,f)) + 1) by A8, NAT_1: 13;

      then

       A11: (( Index (p,f)) + 1) in ( dom f) by A5, FINSEQ_3: 25;

      then

       A12: (( mid (f,(( Index (p,f)) + 1),( len f))) /. 1) = (f /. (( Index (p,f)) + 1)) by A7, SPRECT_2: 8;

      per cases ;

        suppose

         A13: ((( Index (p,f)) + 1) + 1) <= ( len f);

        then ( LSeg (f,(( Index (p,f)) + 1))) = ( LSeg ((f /. (( Index (p,f)) + 1)),(f /. (( Index (p,f)) + (1 + 1))))) by A10, TOPREAL1:def 3;

        then

         A14: (( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) /\ ( LSeg ((f /. (( Index (p,f)) + 1)),(f /. (( Index (p,f)) + (1 + 1)))))) = {(f /. (( Index (p,f)) + 1))} by A1, A8, A9, A13, TOPREAL1:def 6;

        

         A15: (( len f) - (( Index (p,f)) + 1)) >= 0 by A5, XREAL_1: 19;

        (( Index (p,f)) + (1 + 1)) <= ( len f) by A13;

        then

         A16: 2 <= (( len f) - ( Index (p,f))) by XREAL_1: 19;

        

         A17: (f /. (( Index (p,f)) + 1)) in ( LSeg ((f /. (( Index (p,f)) + 1)),(f /. (( Index (p,f)) + (1 + 1))))) by RLTOPSP1: 68;

        (f /. (( Index (p,f)) + 1)) in ( LSeg (p,(f /. (( Index (p,f)) + 1)))) by RLTOPSP1: 68;

        then (f /. (( Index (p,f)) + 1)) in (( LSeg (p,(f /. (( Index (p,f)) + 1)))) /\ ( LSeg ((f /. (( Index (p,f)) + 1)),(f /. (( Index (p,f)) + (1 + 1)))))) by A17, XBOOLE_0:def 4;

        then

         A18: {(f /. (( Index (p,f)) + 1))} c= (( LSeg (p,(f /. (( Index (p,f)) + 1)))) /\ ( LSeg ((f /. (( Index (p,f)) + 1)),(f /. (( Index (p,f)) + (1 + 1)))))) by ZFMISC_1: 31;

        ((2 + (( Index (p,f)) + 1)) - 1) = ((( Index (p,f)) + 1) + 1);

        then

         A19: ((2 + (( Index (p,f)) + 1)) - 1) >= 0 by NAT_1: 2;

        

         A20: ( len ( mid (f,(( Index (p,f)) + 1),( len f)))) = ((( len f) -' (( Index (p,f)) + 1)) + 1) by A6, A10, A5, FINSEQ_6: 118

        .= ((( len f) - (( Index (p,f)) + 1)) + 1) by A15, XREAL_0:def 2

        .= (( len f) - ( Index (p,f)));

        then 2 in ( dom ( mid (f,(( Index (p,f)) + 1),( len f)))) by A16, FINSEQ_3: 25;

        

        then (( mid (f,(( Index (p,f)) + 1),( len f))) /. 2) = (f /. ((2 + (( Index (p,f)) + 1)) -' 1)) by A5, A11, A7, SPRECT_2: 3

        .= (f /. (( Index (p,f)) + (1 + 1))) by A19, XREAL_0:def 2;

        then

         A21: ( LSeg (( mid (f,(( Index (p,f)) + 1),( len f))),1)) = ( LSeg ((f /. (( Index (p,f)) + 1)),(f /. (( Index (p,f)) + (1 + 1))))) by A12, A20, A16, TOPREAL1:def 3;

        (f /. (( Index (p,f)) + 1)) in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by RLTOPSP1: 68;

        then (( LSeg (p,(f /. (( Index (p,f)) + 1)))) /\ ( LSeg ((f /. (( Index (p,f)) + 1)),(f /. (( Index (p,f)) + (1 + 1)))))) c= {(f /. (( Index (p,f)) + 1))} by A4, A14, TOPREAL1: 6, XBOOLE_1: 26;

        then

         A22: (( LSeg (p,(f /. (( Index (p,f)) + 1)))) /\ ( LSeg ((f /. (( Index (p,f)) + 1)),(f /. (( Index (p,f)) + (1 + 1)))))) = {(f /. (( Index (p,f)) + 1))} by A18;

        now

          per cases ;

            suppose p <> (f . (( Index (p,f)) + 1));

            then ( L_Cut (f,p)) = ( <*p*> ^ ( mid (f,(( Index (p,f)) + 1),( len f)))) by JORDAN3:def 3;

            hence thesis by A1, A12, A21, A22, Th28, SPPOL_2: 29;

          end;

            suppose p = (f . (( Index (p,f)) + 1));

            hence thesis by A2, JORDAN3:def 3;

          end;

        end;

        hence thesis;

      end;

        suppose

         A23: ((( Index (p,f)) + 1) + 1) > ( len f);

        

         A24: (( Index (p,f)) + 1) < ( len f) or (( Index (p,f)) + 1) = ( len f) by A5, XXREAL_0: 1;

        now

          per cases ;

            suppose p <> (f . (( Index (p,f)) + 1));

            

            then ( L_Cut (f,p)) = ( <*p*> ^ ( mid (f,( len f),( len f)))) by A23, A24, JORDAN3:def 3, NAT_1: 13

            .= ( <*p*> ^ <*(f . ( len f))*>) by A7, JORDAN4: 15

            .= ( <*p*> ^ <*(f /. ( len f))*>) by A7, PARTFUN1:def 6

            .= <*p, (f /. ( len f))*> by FINSEQ_1:def 9;

            then ( len ( L_Cut (f,p))) = 2 by FINSEQ_1: 44;

            hence thesis by SPPOL_2: 26;

          end;

            suppose p = (f . (( Index (p,f)) + 1));

            

            then ( L_Cut (f,p)) = ( mid (f,( len f),( len f))) by A23, A24, JORDAN3:def 3, NAT_1: 13

            .= <*(f . ( len f))*> by A7, JORDAN4: 15;

            then ( len ( L_Cut (f,p))) = 1 by FINSEQ_1: 39;

            hence thesis by SPPOL_2: 26;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: JORDAN23:33

    

     Th33: for f be FinSequence of ( TOP-REAL 2) st f is unfolded holds for p be Point of ( TOP-REAL 2) st p in ( L~ f) holds ( R_Cut (f,p)) is unfolded

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is unfolded;

      let p be Point of ( TOP-REAL 2);

      assume

       A2: p in ( L~ f);

      then

       A3: 1 <= ( Index (p,f)) by JORDAN3: 8;

      ( len f) <> 0 by A2, TOPREAL1: 22;

      then ( len f) > 0 by NAT_1: 3;

      then

       A4: ( len f) >= ( 0 + 1) by NAT_1: 13;

      then 1 in ( Seg ( len f)) by FINSEQ_1: 1;

      then

       A5: 1 in ( dom f) by FINSEQ_1:def 3;

      

       A6: ( Index (p,f)) < ( len f) by A2, JORDAN3: 8;

      then

       A7: ((( Index (p,f)) + 1) + 0 ) <= ( len f) by NAT_1: 13;

      then

       A8: ( LSeg (f,( Index (p,f)))) = ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A3, TOPREAL1:def 3;

      ( Index (p,f)) in ( Seg ( len f)) by A3, A6, FINSEQ_1: 1;

      then

       A9: ( Index (p,f)) in ( dom f) by FINSEQ_1:def 3;

      then

       A10: (( mid (f,1,( Index (p,f)))) /. ( len ( mid (f,1,( Index (p,f)))))) = (f /. ( Index (p,f))) by A5, SPRECT_2: 9;

      

       A11: p in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A2, JORDAN5B: 29;

      

       A12: ((( Index (p,f)) -' 1) + 1) = ( Index (p,f)) by A2, JORDAN3: 8, XREAL_1: 235;

      per cases by A3, XXREAL_0: 1;

        suppose

         A13: ( Index (p,f)) > ( 0 + 1);

        

         A14: (f /. ( Index (p,f))) in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by RLTOPSP1: 68;

        

         A15: (f /. ( Index (p,f))) in ( LSeg ((f /. ( Index (p,f))),p)) by RLTOPSP1: 68;

        (f /. ( Index (p,f))) in ( LSeg ((f /. (( Index (p,f)) -' 1)),(f /. ( Index (p,f))))) by RLTOPSP1: 68;

        then (f /. ( Index (p,f))) in (( LSeg ((f /. (( Index (p,f)) -' 1)),(f /. ( Index (p,f))))) /\ ( LSeg ((f /. ( Index (p,f))),p))) by A15, XBOOLE_0:def 4;

        then

         A16: {(f /. ( Index (p,f)))} c= (( LSeg ((f /. (( Index (p,f)) -' 1)),(f /. ( Index (p,f))))) /\ ( LSeg ((f /. ( Index (p,f))),p))) by ZFMISC_1: 31;

        

         A17: ((( Index (p,f)) -' 1) + (1 + 1)) <= ( len f) by A7, A12;

        (( Index (p,f)) - 1) > 0 by A13, XREAL_1: 20;

        then (( Index (p,f)) -' 1) > 0 by XREAL_0:def 2;

        then

         A18: (( Index (p,f)) -' 1) >= ( 0 + 1) by NAT_1: 13;

        then ( LSeg (f,(( Index (p,f)) -' 1))) = ( LSeg ((f /. (( Index (p,f)) -' 1)),(f /. ( Index (p,f))))) by A6, A12, TOPREAL1:def 3;

        then (( LSeg ((f /. (( Index (p,f)) -' 1)),(f /. ( Index (p,f))))) /\ ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))))) = {(f /. ( Index (p,f)))} by A1, A12, A8, A18, A17, TOPREAL1:def 6;

        then (( LSeg ((f /. (( Index (p,f)) -' 1)),(f /. ( Index (p,f))))) /\ ( LSeg ((f /. ( Index (p,f))),p))) c= {(f /. ( Index (p,f)))} by A11, A14, TOPREAL1: 6, XBOOLE_1: 26;

        then

         A19: (( LSeg ((f /. (( Index (p,f)) -' 1)),(f /. ( Index (p,f))))) /\ ( LSeg ((f /. ( Index (p,f))),p))) = {(f /. ( Index (p,f)))} by A16;

        

         A20: ( len ( mid (f,1,( Index (p,f))))) = ((( Index (p,f)) -' 1) + 1) by A4, A3, A6, FINSEQ_6: 118

        .= ( Index (p,f)) by A2, JORDAN3: 8, XREAL_1: 235;

        then

         A21: ((( len ( mid (f,1,( Index (p,f))))) -' 1) + 1) = ( len ( mid (f,1,( Index (p,f))))) by A2, JORDAN3: 8, XREAL_1: 235;

        (( len ( mid (f,1,( Index (p,f))))) -' 1) <= ( len ( mid (f,1,( Index (p,f))))) by NAT_D: 35;

        then (( len ( mid (f,1,( Index (p,f))))) -' 1) in ( Seg ( len ( mid (f,1,( Index (p,f)))))) by A18, A20, FINSEQ_1: 1;

        then (( len ( mid (f,1,( Index (p,f))))) -' 1) in ( dom ( mid (f,1,( Index (p,f))))) by FINSEQ_1:def 3;

        

        then

         A22: (( mid (f,1,( Index (p,f)))) /. (( len ( mid (f,1,( Index (p,f))))) -' 1)) = (f /. (((( len ( mid (f,1,( Index (p,f))))) -' 1) + 1) -' 1)) by A2, A9, A5, JORDAN3: 8, SPRECT_2: 3

        .= (f /. (( len ( mid (f,1,( Index (p,f))))) -' 1)) by NAT_D: 34

        .= (f /. (((( Index (p,f)) -' 1) + 1) -' 1)) by A3, A6, JORDAN4: 8

        .= (f /. (( Index (p,f)) -' 1)) by A2, JORDAN3: 8, XREAL_1: 235;

        ((( len ( mid (f,1,( Index (p,f))))) -' 1) + 1) = ( len ( mid (f,1,( Index (p,f))))) by A2, A20, JORDAN3: 8, XREAL_1: 235;

        then

         A23: ( LSeg (( mid (f,1,( Index (p,f)))),(( len ( mid (f,1,( Index (p,f))))) -' 1))) = ( LSeg ((f /. (( Index (p,f)) -' 1)),(f /. ( Index (p,f))))) by A10, A18, A20, A22, TOPREAL1:def 3;

        now

          per cases ;

            suppose p <> (f . 1);

            then ( R_Cut (f,p)) = (( mid (f,1,( Index (p,f)))) ^ <*p*>) by JORDAN3:def 4;

            hence thesis by A1, A10, A23, A21, A19, Th28, SPPOL_2: 30;

          end;

            suppose p = (f . 1);

            then ( R_Cut (f,p)) = <*p*> by JORDAN3:def 4;

            then ( len ( R_Cut (f,p))) = 1 by FINSEQ_1: 39;

            hence thesis by SPPOL_2: 26;

          end;

        end;

        hence thesis;

      end;

        suppose

         A24: ( Index (p,f)) = ( 0 + 1);

        now

          per cases ;

            suppose p <> (f . 1);

            

            then ( R_Cut (f,p)) = (( mid (f,1,1)) ^ <*p*>) by A24, JORDAN3:def 4

            .= ( <*(f . 1)*> ^ <*p*>) by A5, JORDAN4: 15

            .= ( <*(f /. 1)*> ^ <*p*>) by A5, PARTFUN1:def 6

            .= <*(f /. 1), p*> by FINSEQ_1:def 9;

            then ( len ( R_Cut (f,p))) = 2 by FINSEQ_1: 44;

            hence thesis by SPPOL_2: 26;

          end;

            suppose p = (f . 1);

            then ( R_Cut (f,p)) = <*p*> by JORDAN3:def 4;

            then ( len ( R_Cut (f,p))) = 1 by FINSEQ_1: 39;

            hence thesis by SPPOL_2: 26;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: JORDAN23:34

    for f be FinSequence of ( TOP-REAL 2) st f is unfolded weakly-one-to-one holds for p,q be Point of ( TOP-REAL 2) st p in ( L~ f) & q in ( L~ f) holds ( B_Cut (f,p,q)) is unfolded

    proof

      let f be FinSequence of ( TOP-REAL 2);

      assume

       A1: f is unfolded weakly-one-to-one;

      let p,q be Point of ( TOP-REAL 2);

      assume that

       A2: p in ( L~ f) and

       A3: q in ( L~ f);

      

       A4: ( Index (p,f)) < ( len f) by A2, JORDAN3: 8;

      

       A5: 1 <= ( Index (p,f)) by A2, JORDAN3: 8;

      then ( Index (p,f)) in ( Seg ( len f)) by A4, FINSEQ_1: 1;

      then

       A6: ( Index (p,f)) in ( dom f) by FINSEQ_1:def 3;

      per cases ;

        suppose

         A7: p <> q;

        now

          per cases ;

            suppose

             A8: p in ( L~ f) & q in ( L~ f) & ( Index (p,f)) < ( Index (q,f));

            then

             A9: q in ( L~ ( L_Cut (f,p))) by JORDAN3: 29;

            ( L_Cut (f,p)) is unfolded by A1, A2, Th32;

            then ( R_Cut (( L_Cut (f,p)),q)) is unfolded by A9, Th33;

            hence thesis by A8, JORDAN3:def 7;

          end;

            suppose

             A10: ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

            

             A11: ( L_Cut (f,p)) is unfolded by A1, A2, Th32;

            q in ( L~ ( L_Cut (f,p))) by A2, A3, A7, A10, JORDAN3: 31;

            then ( R_Cut (( L_Cut (f,p)),q)) is unfolded by A11, Th33;

            hence thesis by A10, JORDAN3:def 7;

          end;

            suppose

             A12: not (p in ( L~ f) & q in ( L~ f) & ( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

             A13:

            now

              per cases by A2, A3, A12, XXREAL_0: 1;

                suppose ( Index (q,f)) < ( Index (p,f));

                hence p in ( L~ ( L_Cut (f,q))) by A2, A3, JORDAN3: 29;

              end;

                suppose

                 A14: ( Index (q,f)) = ( Index (p,f));

                

                 A15: (( Index (p,f)) + 1) >= 1 by NAT_1: 11;

                (( Index (p,f)) + 1) <= ( len f) by A4, NAT_1: 13;

                then (( Index (p,f)) + 1) in ( Seg ( len f)) by A15, FINSEQ_1: 1;

                then

                 A16: (( Index (p,f)) + 1) in ( dom f) by FINSEQ_1:def 3;

                set Ls = ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

                

                 A17: q in Ls by A3, A14, JORDAN5B: 29;

                

                 A18: p in Ls by A2, JORDAN5B: 29;

                (f . ( Index (p,f))) <> (f . (( Index (p,f)) + 1)) by A1, A5, A4;

                then (f . ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A16, PARTFUN1:def 6;

                then

                 A19: (f /. ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A6, PARTFUN1:def 6;

                then

                 A20: Ls is_an_arc_of ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by TOPREAL1: 9;

                 not LE (p,q,Ls,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A12, A14, A19, JORDAN5C: 17;

                then LE (q,p,Ls,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A7, A20, A18, A17, JORDAN5C: 14;

                hence p in ( L~ ( L_Cut (f,q))) by A2, A3, A7, A14, A19, JORDAN3: 31, JORDAN5C: 17;

              end;

            end;

            

             A21: ( B_Cut (f,p,q)) = ( Rev ( R_Cut (( L_Cut (f,q)),p))) by A12, JORDAN3:def 7;

            ( L_Cut (f,q)) is unfolded by A1, A3, Th32;

            then ( R_Cut (( L_Cut (f,q)),p)) is unfolded by A13, Th33;

            hence thesis by A21, SPPOL_2: 28;

          end;

        end;

        hence thesis;

      end;

        suppose p = q;

        then ( B_Cut (f,p,q)) = <*p*> by A1, A2, Th15;

        then ( len ( B_Cut (f,p,q))) = 1 by FINSEQ_1: 39;

        hence thesis by SPPOL_2: 26;

      end;

    end;

    theorem :: JORDAN23:35

    

     Th35: for f,g be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st f is almost-one-to-one special unfolded s.n.c. & p in ( L~ f) & p <> (f . 1) & g = (( mid (f,1,( Index (p,f)))) ^ <*p*>) holds g is_S-Seq_joining ((f /. 1),p)

    proof

      let f,g be FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2);

      assume that

       A1: f is almost-one-to-one special unfolded s.n.c. and

       A2: p in ( L~ f) and

       A3: p <> (f . 1) and

       A4: g = (( mid (f,1,( Index (p,f)))) ^ <*p*>);

      

       A5: ( Index (p,f)) < ( len f) by A2, JORDAN3: 8;

      

       A6: for j1,j2 be Nat st (j1 + 1) < j2 holds ( LSeg (g,j1)) misses ( LSeg (g,j2))

      proof

        let j1,j2 be Nat;

        assume

         A7: (j1 + 1) < j2;

        j1 >= 0 by NAT_1: 2;

        then

         A8: j1 = 0 or j1 >= ( 0 + 1) by NAT_1: 13;

        now

          per cases by A8, XXREAL_0: 1;

            case j1 = 0 ;

            then ( LSeg (g,j1)) = {} by TOPREAL1:def 3;

            then (( LSeg (g,j1)) /\ ( LSeg (g,j2))) = {} ;

            hence thesis;

          end;

            case that

             A9: j1 = 1 or j1 > 1 and

             A10: (j2 + 1) <= ( len g);

            j2 < ( len g) by A10, NAT_1: 13;

            then (j1 + 1) < ( len g) by A7, XXREAL_0: 2;

            then

             A11: ( LSeg (g,j1)) c= ( LSeg (f,j1)) by A2, A4, A9, JORDAN3: 18;

            (1 + 1) <= (j1 + 1) by A9, XREAL_1: 6;

            then 2 <= j2 by A7, XXREAL_0: 2;

            then 1 <= j2 by XXREAL_0: 2;

            then

             A12: ( LSeg (g,j2)) c= ( LSeg (f,j2)) by A2, A4, A10, JORDAN3: 18;

            ( LSeg (f,j1)) misses ( LSeg (f,j2)) by A1, A7, TOPREAL1:def 7;

            then (( LSeg (f,j1)) /\ ( LSeg (f,j2))) = {} ;

            then (( LSeg (g,j1)) /\ ( LSeg (g,j2))) = {} by A11, A12, XBOOLE_1: 3, XBOOLE_1: 27;

            hence thesis;

          end;

            case (j2 + 1) > ( len g);

            then ( LSeg (g,j2)) = {} by TOPREAL1:def 3;

            then (( LSeg (g,j1)) /\ ( LSeg (g,j2))) = {} ;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A13: ( len g) = (( len ( mid (f,1,( Index (p,f))))) + ( len <*p*>)) by A4, FINSEQ_1: 22

      .= (( len ( mid (f,1,( Index (p,f))))) + 1) by FINSEQ_1: 39;

      consider i be Nat such that 1 <= i and

       A14: (i + 1) <= ( len f) and p in ( LSeg (f,i)) by A2, SPPOL_2: 13;

      

       A15: 1 <= ( Index (p,f)) by A2, JORDAN3: 8;

      1 <= (1 + i) by NAT_1: 12;

      then

       A16: 1 <= ( len f) by A14, XXREAL_0: 2;

      then

       A17: ( len ( mid (f,1,( Index (p,f))))) = ((( Index (p,f)) -' 1) + 1) by A15, A5, FINSEQ_6: 118;

      then

       A18: ( len ( mid (f,1,( Index (p,f))))) = ( Index (p,f)) by A2, JORDAN3: 8, XREAL_1: 235;

      then (g . 1) = (( mid (f,1,( Index (p,f)))) . 1) by A4, A15, FINSEQ_6: 109;

      then (g . 1) = (f . 1) by A15, A5, A16, FINSEQ_6: 118;

      then

       A19: (g . 1) = (f /. 1) by A16, FINSEQ_4: 15;

      

       A20: for j be Nat st 1 <= j & (j + 2) <= ( len g) holds (( LSeg (g,j)) /\ ( LSeg (g,(j + 1)))) = {(g /. (j + 1))}

      proof

        let j be Nat;

        assume that

         A21: 1 <= j and

         A22: (j + 2) <= ( len g);

        

         A23: (j + 1) <= ( len g) by A22, NAT_D: 47;

        then ( LSeg (g,j)) = ( LSeg ((g /. j),(g /. (j + 1)))) by A21, TOPREAL1:def 3;

        then

         A24: (g /. (j + 1)) in ( LSeg (g,j)) by RLTOPSP1: 68;

        

         A25: 1 <= (j + 1) by A21, NAT_D: 48;

        then ( LSeg (g,(j + 1))) = ( LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1)))) by A22, TOPREAL1:def 3;

        then (g /. (j + 1)) in ( LSeg (g,(j + 1))) by RLTOPSP1: 68;

        then (g /. (j + 1)) in (( LSeg (g,j)) /\ ( LSeg (g,(j + 1)))) by A24, XBOOLE_0:def 4;

        then

         A26: {(g /. (j + 1))} c= (( LSeg (g,j)) /\ ( LSeg (g,(j + 1)))) by ZFMISC_1: 31;

        (j + 1) <= ( len g) by A22, NAT_D: 47;

        then

         A27: ( LSeg (g,j)) c= ( LSeg (f,j)) by A2, A4, A21, JORDAN3: 18;

        

         A28: ( Index (p,f)) <= ( len f) by A2, JORDAN3: 8;

        

         A29: ((j + 1) + 1) <= ( len g) by A22;

        then ( LSeg (g,(j + 1))) c= ( LSeg (f,(j + 1))) by A2, A4, A25, JORDAN3: 18;

        then

         A30: (( LSeg (g,j)) /\ ( LSeg (g,(j + 1)))) c= (( LSeg (f,j)) /\ ( LSeg (f,(j + 1)))) by A27, XBOOLE_1: 27;

        

         A31: (g /. (j + 1)) = (g . (j + 1)) by A25, A23, FINSEQ_4: 15;

        now

          

           A32: ( len g) = (( len ( mid (f,1,( Index (p,f))))) + 1) by A4, FINSEQ_2: 16;

          ( Index (p,f)) <= ( len f) by A2, JORDAN3: 8;

          then

           A33: ( len g) <= (( len f) + 1) by A18, A32, XREAL_1: 6;

          now

            per cases by A33, XXREAL_0: 1;

              case ( len g) = (( len f) + 1);

              hence contradiction by A2, A18, A32, JORDAN3: 8;

            end;

              case ( len g) < (( len f) + 1);

              then ( len g) <= ( len f) by NAT_1: 13;

              then (j + 2) <= ( len f) by A22, XXREAL_0: 2;

              then

               A34: (( LSeg (g,j)) /\ ( LSeg (g,(j + 1)))) c= {(f /. (j + 1))} by A1, A21, A30, TOPREAL1:def 6;

              

               A35: (j + 1) <= ( Index (p,f)) by A18, A29, A32, XREAL_1: 6;

              then (j + 1) <= ( len f) by A28, XXREAL_0: 2;

              then

               A36: (f . (j + 1)) = (f /. (j + 1)) by A25, FINSEQ_4: 15;

              (g . (j + 1)) = (( mid (f,1,( Index (p,f)))) . (j + 1)) by A4, A18, A25, A35, FINSEQ_1: 64

              .= (f . (j + 1)) by A5, A25, A35, FINSEQ_6: 123;

              hence thesis by A31, A26, A34, A36;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      for j be Nat st 1 <= j & (j + 1) <= ( len g) holds ((g /. j) `1 ) = ((g /. (j + 1)) `1 ) or ((g /. j) `2 ) = ((g /. (j + 1)) `2 )

      proof

        

         A37: ( Index (p,f)) < ( len f) by A2, JORDAN3: 8;

        let j be Nat;

        assume that

         A38: 1 <= j and

         A39: (j + 1) <= ( len g);

        

         A40: ( LSeg (g,j)) = ( LSeg ((g /. j),(g /. (j + 1)))) by A38, A39, TOPREAL1:def 3;

        (j + 1) <= (( Index (p,f)) + 1) by A4, A18, A39, FINSEQ_2: 16;

        then j <= ( Index (p,f)) by XREAL_1: 6;

        then j < ( len f) by A37, XXREAL_0: 2;

        then

         A41: (j + 1) <= ( len f) by NAT_1: 13;

        then

         A42: ( LSeg (f,j)) = ( LSeg ((f /. j),(f /. (j + 1)))) by A38, TOPREAL1:def 3;

        

         A43: ((f /. j) `1 ) = ((f /. (j + 1)) `1 ) or ((f /. j) `2 ) = ((f /. (j + 1)) `2 ) by A1, A38, A41, TOPREAL1:def 5;

        ( LSeg (g,j)) c= ( LSeg (f,j)) by A2, A4, A38, A39, JORDAN3: 18;

        hence thesis by A40, A42, A43, JORDAN3: 3;

      end;

      then

       A44: g is unfolded s.n.c. special by A20, A6, TOPREAL1:def 5, TOPREAL1:def 6, TOPREAL1:def 7;

      1 <= ( len <*p*>) by FINSEQ_1: 39;

      then

       A45: 1 in ( dom <*p*>) by FINSEQ_3: 25;

      for x1,x2 be object st x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume that

         A46: x1 in ( dom g) and

         A47: x2 in ( dom g) and

         A48: (g . x1) = (g . x2);

        reconsider n1 = x1, n2 = x2 as Nat by A46, A47;

        

         A49: 1 <= n1 by A46, FINSEQ_3: 25;

        

         A50: n2 <= ( len g) by A47, FINSEQ_3: 25;

        

         A51: 1 <= n2 by A47, FINSEQ_3: 25;

        

         A52: n1 <= ( len g) by A46, FINSEQ_3: 25;

        now

          

           A53: (g . ( len g)) = ( <*p*> . 1) by A4, A45, A13, FINSEQ_1:def 7

          .= p by FINSEQ_1:def 8;

          now

            per cases ;

              case

               A54: n1 = ( len g);

              now

                assume

                 A55: n2 <> ( len g);

                then n2 < ( len g) by A50, XXREAL_0: 1;

                then

                 A56: n2 <= ( len ( mid (f,1,( Index (p,f))))) by A13, NAT_1: 13;

                then

                 A57: n2 < ( len f) by A5, A18, XXREAL_0: 2;

                (g . n2) = (( mid (f,1,( Index (p,f)))) . n2) by A4, A51, A56, FINSEQ_1: 64;

                then (g . n2) = (f . ((n2 + 1) -' 1)) by A15, A5, A16, A51, A56, FINSEQ_6: 118;

                then

                 A58: p = (f . n2) by A48, A53, A54, NAT_D: 34;

                then 1 < n2 by A3, A51, XXREAL_0: 1;

                then (( Index (p,f)) + 1) = n2 by A1, A58, A57, Th18;

                hence contradiction by A2, A17, A13, A55, JORDAN3: 8, XREAL_1: 235;

              end;

              hence thesis by A54;

            end;

              case

               A59: n2 = ( len g);

              now

                assume

                 A60: n1 <> ( len g);

                then n1 < ( len g) by A52, XXREAL_0: 1;

                then

                 A61: n1 <= ( len ( mid (f,1,( Index (p,f))))) by A13, NAT_1: 13;

                then

                 A62: n1 < ( len f) by A5, A18, XXREAL_0: 2;

                (g . n1) = (( mid (f,1,( Index (p,f)))) . n1) by A4, A49, A61, FINSEQ_1: 64;

                then (g . n1) = (f . ((n1 + 1) -' 1)) by A15, A5, A16, A49, A61, FINSEQ_6: 118;

                then

                 A63: p = (f . n1) by A48, A53, A59, NAT_D: 34;

                then 1 < n1 by A3, A49, XXREAL_0: 1;

                then (( Index (p,f)) + 1) = n1 by A1, A63, A62, Th18;

                hence contradiction by A2, A17, A13, A60, JORDAN3: 8, XREAL_1: 235;

              end;

              hence thesis by A59;

            end;

              case that

               A64: n1 <> ( len g) and

               A65: n2 <> ( len g);

              n2 < ( len g) by A50, A65, XXREAL_0: 1;

              then

               A66: n2 <= ( len ( mid (f,1,( Index (p,f))))) by A13, NAT_1: 13;

              

              then

               A67: (g . n2) = (( mid (f,1,( Index (p,f)))) . n2) by A4, A51, FINSEQ_1: 64

              .= (f . n2) by A5, A18, A51, A66, FINSEQ_6: 123;

              n2 < ( len f) by A5, A18, A66, XXREAL_0: 2;

              then n2 in ( Seg ( len f)) by A51, FINSEQ_1: 1;

              then

               A68: n2 in ( dom f) by FINSEQ_1:def 3;

              n1 < ( len g) by A52, A64, XXREAL_0: 1;

              then

               A69: n1 <= ( len ( mid (f,1,( Index (p,f))))) by A13, NAT_1: 13;

              then n1 < ( len f) by A5, A18, XXREAL_0: 2;

              then n1 in ( Seg ( len f)) by A49, FINSEQ_1: 1;

              then

               A70: n1 in ( dom f) by FINSEQ_1:def 3;

              (g . n1) = (( mid (f,1,( Index (p,f)))) . n1) by A4, A49, A69, FINSEQ_1: 64

              .= (f . n1) by A5, A18, A49, A69, FINSEQ_6: 123;

              hence thesis by A1, A5, A18, A48, A69, A66, A67, A70, A68;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      then

       A71: g is one-to-one;

      (1 + 1) <= ( len g) by A15, A18, A13, XREAL_1: 6;

      then

       A72: g is being_S-Seq by A71, A44, TOPREAL1:def 8;

      (g . ( len g)) = p by A4, A13, FINSEQ_1: 42;

      hence thesis by A19, A72, JORDAN3:def 2;

    end;

    theorem :: JORDAN23:36

    

     Th36: for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st f is poorly-one-to-one unfolded s.n.c. & p in ( L~ f) & p = (f . (( Index (p,f)) + 1)) & p <> (f . ( len f)) holds ((( Index (p,( Rev f))) + ( Index (p,f))) + 1) = ( len f)

    proof

      let f be FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2) such that

       A1: f is poorly-one-to-one unfolded s.n.c. and

       A2: p in ( L~ f) and

       A3: p = (f . (( Index (p,f)) + 1)) and

       A4: p <> (f . ( len f));

      

       A5: ( Rev f) is s.n.c. by A1, SPPOL_2: 35;

      

       A6: ( len f) = ( len ( Rev f)) by FINSEQ_5:def 3;

      ( len f) <= (( len f) + ( Index (p,f))) by NAT_1: 11;

      then

       A7: (( len f) - ( Index (p,f))) <= ( len ( Rev f)) by A6, XREAL_1: 20;

      ( Index (p,f)) <= ( len f) by A2, JORDAN3: 8;

      then

       A8: (( len f) - ( Index (p,f))) = (( len f) -' ( Index (p,f))) by XREAL_1: 233;

      ( Index (p,f)) < ( len f) by A2, JORDAN3: 8;

      then

       A9: (( Index (p,f)) + 1) <= ( len f) by NAT_1: 13;

      then (( Index (p,f)) + 1) < ( len f) by A3, A4, XXREAL_0: 1;

      then

       A10: 1 < (( len f) - ( Index (p,f))) by XREAL_1: 20;

      1 <= (( Index (p,f)) + 1) by NAT_1: 11;

      then (( Index (p,f)) + 1) in ( dom f) by A9, FINSEQ_3: 25;

      then

       A11: (( Index (p,f)) + 1) in ( dom ( Rev f)) by FINSEQ_5: 57;

      p = (( Rev ( Rev f)) . (( Index (p,f)) + 1)) by A3

      .= (( Rev f) . ((( len ( Rev f)) - (( Index (p,f)) + 1)) + 1)) by A11, FINSEQ_5: 58

      .= (( Rev f) . (( len ( Rev f)) - ( Index (p,f))))

      .= (( Rev f) . (( len f) - ( Index (p,f)))) by FINSEQ_5:def 3;

      then (( Index (p,( Rev f))) + 1) = (( len f) -' ( Index (p,f))) by A1, A5, A7, A10, A8, Th18, SPPOL_2: 28;

      hence thesis by A8;

    end;

    theorem :: JORDAN23:37

    for f be non empty FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st f is weakly-one-to-one & ( len f) >= 2 holds ( L_Cut (f,(f /. 1))) = f

    proof

      let f be non empty FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2);

      assume that

       A1: f is weakly-one-to-one and

       A2: ( len f) >= 2;

      

       A3: ( Index ((f /. 1),f)) = 1 by A2, JORDAN3: 11;

      1 <= ( len f) by A2, XXREAL_0: 2;

      then

       A4: 1 in ( dom f) by FINSEQ_3: 25;

      then

       A5: (f /. 1) = (f . 1) by PARTFUN1:def 6;

      2 = (1 + 1);

      then

       A6: 1 < ( len f) by A2, NAT_1: 13;

      then (f . 1) <> (f . (1 + 1)) by A1;

      then (f /. 1) <> (f . (1 + 1)) by A4, PARTFUN1:def 6;

      

      hence ( L_Cut (f,(f /. 1))) = ( <*(f /. 1)*> ^ ( mid (f,(( Index ((f /. 1),f)) + 1),( len f)))) by A3, JORDAN3:def 3

      .= ( mid (f,1,( len f))) by A4, A6, A5, A3, FINSEQ_6: 126

      .= f by A2, FINSEQ_6: 120, XXREAL_0: 2;

    end;

    theorem :: JORDAN23:38

    

     Th38: for f be non empty FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st f is poorly-one-to-one unfolded s.n.c. & p in ( L~ f) & p <> (f . ( len f)) holds ( L_Cut (( Rev f),p)) = ( Rev ( R_Cut (f,p)))

    proof

      let f be non empty FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2) such that

       A1: f is poorly-one-to-one unfolded s.n.c. and

       A2: p in ( L~ f) and

       A3: p <> (f . ( len f));

      

       A4: ( Index (p,f)) < ( len f) by A2, JORDAN3: 8;

      

       A5: p in ( L~ ( Rev f)) by A2, SPPOL_2: 22;

      

       A6: ( Rev f) is s.n.c. by A1, SPPOL_2: 35;

      

       A7: ( dom ( Rev f)) = ( dom f) by FINSEQ_5: 57;

      

       A8: ( len f) = ( len ( Rev f)) by FINSEQ_5:def 3;

      

       A9: 1 <= ( Index (p,f)) by A2, JORDAN3: 8;

      then

       A10: 1 < ( len f) by A4, XXREAL_0: 2;

      ( L~ f) = ( L~ ( Rev f)) by SPPOL_2: 22;

      then ( Index (p,( Rev f))) < ( len ( Rev f)) by A2, JORDAN3: 8;

      then

       A11: (( Index (p,( Rev f))) + 1) <= ( len f) by A8, NAT_1: 13;

      1 <= (( Index (p,( Rev f))) + 1) by NAT_1: 11;

      then

       A12: (( Index (p,( Rev f))) + 1) in ( dom f) by A11, FINSEQ_3: 25;

      per cases by A3;

        suppose

         A13: p = (f . 1);

        

         A14: ((( len ( Rev f)) -' 1) + 1) = ( len ( Rev f)) by A8, A9, A4, XREAL_1: 235, XXREAL_0: 2;

        then

         A15: ((( Rev f) /^ (( len ( Rev f)) -' 1)) . 1) = (( Rev f) . ( len ( Rev f))) by FINSEQ_6: 114;

        

         A16: ( len (( Rev f) /^ (( len ( Rev f)) -' 1))) = (( len ( Rev f)) -' (( len ( Rev f)) -' 1)) by RFINSEQ: 29;

        

         A17: 1 <= (( len ( Rev f)) - (( len ( Rev f)) -' 1)) by A14;

        

         A19: (( Rev f) /^ (( len ( Rev f)) -' 1)) is non empty by A16, A17, NAT_D: 39;

        ((( len ( Rev f)) -' ( len ( Rev f))) + 1) = ((( len ( Rev f)) - ( len ( Rev f))) + 1) by XREAL_1: 233

        .= 1;

        

        then

         A20: ( mid (( Rev f),( len ( Rev f)),( len ( Rev f)))) = ((( Rev f) /^ (( len ( Rev f)) -' 1)) | 1) by FINSEQ_6:def 3

        .= <*((( Rev f) /^ (( len ( Rev f)) -' 1)) . 1)*> by A19, FINSEQ_5: 20

        .= <*(( Rev f) . ( len ( Rev f)))*> by A15;

        

         A21: p = (( Rev f) . ( len f)) by A13, FINSEQ_5: 62;

        then (( Index (p,( Rev f))) + 1) = ( len f) by A1, A6, A8, A10, Th18, SPPOL_2: 28;

        

        hence ( L_Cut (( Rev f),p)) = <*p*> by A8, A21, A20, JORDAN3:def 3

        .= ( Rev <*p*>) by FINSEQ_5: 60

        .= ( Rev ( R_Cut (f,p))) by A13, JORDAN3:def 4;

      end;

        suppose that

         A22: p <> (f . 1) and

         A23: p <> (f . ( len f)) and

         A24: p = (f . (( Index (p,f)) + 1));

        

         A25: ( len f) = ((( Index (p,( Rev f))) + ( Index (p,f))) + 1) by A1, A2, A23, A24, Th36

        .= (( Index (p,f)) + (( Index (p,( Rev f))) + 1));

        ( len f) = ((( Index (p,( Rev f))) + ( Index (p,f))) + 1) by A1, A2, A23, A24, Th36

        .= (( Index (p,( Rev f))) + (( Index (p,f)) + 1));

        

        then

         A26: p = (f . ((( len f) - (( Index (p,( Rev f))) + 1)) + 1)) by A24

        .= (( Rev f) . (( Index (p,( Rev f))) + 1)) by A12, FINSEQ_5: 58;

        

         A27: (( len f) -' ( Index (p,f))) = (( len f) - ( Index (p,f))) by A4, XREAL_1: 233

        .= (( Index (p,( Rev f))) + 1) by A25;

        p <> (( Rev f) . ( len f)) by A22, FINSEQ_5: 62;

        then

         A28: (( Index (p,( Rev f))) + 1) < ( len f) by A11, A26, XXREAL_0: 1;

        

        thus ( L_Cut (( Rev f),p)) = ( mid (( Rev f),(( Index (p,( Rev f))) + 1),( len f))) by A8, A26, JORDAN3:def 3

        .= ( <*p*> ^ ( mid (( Rev f),((( len f) -' ( Index (p,f))) + 1),( len f)))) by A7, A12, A26, A27, A28, FINSEQ_6: 126

        .= ( <*p*> ^ ( mid (( Rev f),((( len f) -' ( Index (p,f))) + 1),((( len f) -' 1) + 1)))) by A9, A4, XREAL_1: 235, XXREAL_0: 2

        .= ( <*p*> ^ ( Rev ( mid (f,1,( Index (p,f)))))) by A9, A4, A10, FINSEQ_6: 113

        .= ( Rev (( mid (f,1,( Index (p,f)))) ^ <*p*>)) by FINSEQ_5: 63

        .= ( Rev ( R_Cut (f,p))) by A22, JORDAN3:def 4;

      end;

        suppose that

         A29: p <> (f . 1) and

         A30: p <> (f . (( Index (p,f)) + 1));

        

         A31: p <> (( Rev f) . ( len f)) by A29, FINSEQ_5: 62;

         A32:

        now

          assume

           A33: p = (( Rev f) . (( Index (p,( Rev f))) + 1));

          

          then

           A34: ( len ( Rev f)) = ((( Index (p,( Rev ( Rev f)))) + ( Index (p,( Rev f)))) + 1) by A1, A6, A5, A8, A31, Th36, SPPOL_2: 28

          .= ((( Index (p,f)) + 1) + ( Index (p,( Rev f))));

          p = (f . ((( len f) - (( Index (p,( Rev f))) + 1)) + 1)) by A12, A33, FINSEQ_5: 58

          .= (f . (( Index (p,f)) + 1)) by A8, A34;

          hence contradiction by A30;

        end;

        

         A35: ( Index (p,f)) < ( len f) by A2, JORDAN3: 8;

        ( len f) = (( Index (p,( Rev f))) + ( Index (p,f))) by A1, A2, A30, JORDAN3: 21;

        

        then ( Index (p,( Rev f))) = (( len f) - ( Index (p,f)))

        .= (( len f) -' ( Index (p,f))) by A35, XREAL_1: 233;

        

        hence ( L_Cut (( Rev f),p)) = ( <*p*> ^ ( mid (( Rev f),((( len f) -' ( Index (p,f))) + 1),( len f)))) by A8, A32, JORDAN3:def 3

        .= ( <*p*> ^ ( mid (( Rev f),((( len f) -' ( Index (p,f))) + 1),((( len f) -' 1) + 1)))) by A9, A4, XREAL_1: 235, XXREAL_0: 2

        .= ( <*p*> ^ ( Rev ( mid (f,1,( Index (p,f)))))) by A9, A4, A10, FINSEQ_6: 113

        .= ( Rev (( mid (f,1,( Index (p,f)))) ^ <*p*>)) by FINSEQ_5: 63

        .= ( Rev ( R_Cut (f,p))) by A29, JORDAN3:def 4;

      end;

    end;

    theorem :: JORDAN23:39

    

     Th39: for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st f is almost-one-to-one special unfolded s.n.c. & p in ( L~ f) & p <> (f . 1) holds ( R_Cut (f,p)) is_S-Seq_joining ((f /. 1),p)

    proof

      let f be FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2);

      assume that

       A1: f is almost-one-to-one special unfolded s.n.c. and

       A2: p in ( L~ f) and

       A3: p <> (f . 1);

      ( R_Cut (f,p)) = (( mid (f,1,( Index (p,f)))) ^ <*p*>) by A3, JORDAN3:def 4;

      hence thesis by A1, A2, A3, Th35;

    end;

    theorem :: JORDAN23:40

    

     Th40: for f be non empty FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st f is almost-one-to-one special unfolded s.n.c. & p in ( L~ f) & p <> (f . ( len f)) & p <> (f . 1) holds ( L_Cut (f,p)) is_S-Seq_joining (p,(f /. ( len f)))

    proof

      let f be non empty FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2);

      assume that

       A1: f is almost-one-to-one special unfolded s.n.c. and

       A2: p in ( L~ f) and

       A3: p <> (f . ( len f)) and

       A4: p <> (f . 1);

      

       A5: ( Rev f) is special by A1, SPPOL_2: 40;

      

       A6: p in ( L~ ( Rev f)) by A2, SPPOL_2: 22;

      p <> (( Rev f) . ( len f)) by A4, FINSEQ_5: 62;

      then

       A7: p <> (( Rev f) . ( len ( Rev f))) by FINSEQ_5:def 3;

      

       A8: ( Rev f) is s.n.c. by A1, SPPOL_2: 35;

      

       A9: p <> (( Rev f) . 1) by A3, FINSEQ_5: 62;

      

       A10: ( Rev f) is unfolded by A1, SPPOL_2: 28;

      ( L_Cut (f,p)) = ( L_Cut (( Rev ( Rev f)),p))

      .= ( Rev ( R_Cut (( Rev f),p))) by A1, A7, A10, A8, A6, Th38;

      then ( L_Cut (f,p)) is_S-Seq_joining (p,(( Rev f) /. 1)) by A1, A5, A10, A8, A6, A9, Th39, JORDAN3: 15;

      hence thesis by FINSEQ_5: 65;

    end;

    theorem :: JORDAN23:41

    for f be FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st f is almost-one-to-one special unfolded s.n.c. & p in ( L~ f) & p <> (f . 1) holds ( R_Cut (f,p)) is being_S-Seq

    proof

      let f be FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2);

      assume that

       A1: f is almost-one-to-one special unfolded s.n.c. and

       A2: p in ( L~ f) and

       A3: p <> (f . 1);

      ( R_Cut (f,p)) is_S-Seq_joining ((f /. 1),p) by A1, A2, A3, Th39;

      hence thesis by JORDAN3:def 2;

    end;

    theorem :: JORDAN23:42

    

     Th42: for f be non empty FinSequence of ( TOP-REAL 2) holds for p be Point of ( TOP-REAL 2) st f is almost-one-to-one special unfolded s.n.c. & p in ( L~ f) & p <> (f . ( len f)) & p <> (f . 1) holds ( L_Cut (f,p)) is being_S-Seq

    proof

      let f be non empty FinSequence of ( TOP-REAL 2);

      let p be Point of ( TOP-REAL 2);

      assume that

       A1: f is almost-one-to-one special unfolded s.n.c. and

       A2: p in ( L~ f) and

       A3: p <> (f . ( len f)) and

       A4: p <> (f . 1);

      ( L_Cut (f,p)) is_S-Seq_joining (p,(f /. ( len f))) by A1, A2, A3, A4, Th40;

      hence thesis by JORDAN3:def 2;

    end;

    

     Lm1: for f be non empty FinSequence of ( TOP-REAL 2) holds for p,q be Point of ( TOP-REAL 2) st f is almost-one-to-one special unfolded s.n.c. & p in ( L~ f) & q in ( L~ f) & p <> q & p <> (f . 1) & (( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) holds ( B_Cut (f,p,q)) is_S-Seq_joining (p,q)

    proof

      let f be non empty FinSequence of ( TOP-REAL 2);

      let p,q be Point of ( TOP-REAL 2);

      assume that

       A1: f is almost-one-to-one special unfolded s.n.c. and

       A2: p in ( L~ f) and

       A3: q in ( L~ f) and

       A4: p <> q;

      assume

       A5: p <> (f . 1);

      

       A6: ( Index (q,f)) < ( len f) by A3, JORDAN3: 8;

      ( Index (p,f)) < ( len f) by A2, JORDAN3: 8;

      then

       A7: (( Index (p,f)) + 1) <= ( len f) by NAT_1: 13;

      assume

       A8: ( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

      then

       A9: ( B_Cut (f,p,q)) = ( R_Cut (( L_Cut (f,p)),q)) by A2, A3, JORDAN3:def 7;

      1 <= ( Index (q,f)) by A3, JORDAN3: 8;

      then

       A10: 1 < ( len f) by A6, XXREAL_0: 2;

       A11:

      now

        per cases by A8;

          case

           A12: ( Index (p,f)) < ( Index (q,f));

          assume

           A13: p = (f . ( len f));

          (( Index (p,f)) + 1) <= ( Index (q,f)) by A12, NAT_1: 13;

          then ( len f) <= ( Index (q,f)) by A1, A10, A13, Th18;

          hence contradiction by A3, JORDAN3: 8;

        end;

          case

           A14: ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

           A15:

          now

            q in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A14, JORDAN3:def 5;

            then

            consider r be Real such that

             A16: q = (((1 - r) * (f /. ( Index (p,f)))) + (r * (f /. (( Index (p,f)) + 1)))) and

             A17: 0 <= r and

             A18: r <= 1;

            

             A19: p = (1 * p) by RLVECT_1:def 8

            .= (( 0. ( TOP-REAL 2)) + (1 * p)) by RLVECT_1: 4

            .= (((1 - 1) * (f /. ( Index (p,f)))) + (1 * p)) by RLVECT_1: 10;

            assume

             A20: p = (f . (( Index (p,f)) + 1));

            then p = (f /. (( Index (p,f)) + 1)) by A7, FINSEQ_4: 15, NAT_1: 11;

            then 1 <= r by A14, A16, A17, A19, JORDAN3:def 5;

            then r = 1 by A18, XXREAL_0: 1;

            hence contradiction by A4, A7, A20, A16, A19, FINSEQ_4: 15, NAT_1: 11;

          end;

          assume p = (f . ( len f));

          hence contradiction by A1, A10, A15, Th18;

        end;

      end;

      then ( L_Cut (f,p)) is_S-Seq_joining (p,(f /. ( len f))) by A1, A2, A5, Th40;

      then

       A21: (( L_Cut (f,p)) . 1) = p by JORDAN3:def 2;

      now

        per cases by A8;

          case ( Index (p,f)) < ( Index (q,f));

          then q in ( L~ ( L_Cut (f,p))) by A2, A3, JORDAN3: 29;

          hence ex i1 be Nat st 1 <= i1 & (i1 + 1) <= ( len ( L_Cut (f,p))) & q in ( LSeg (( L_Cut (f,p)),i1)) by SPPOL_2: 13;

        end;

          case ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

          then q in ( L~ ( L_Cut (f,p))) by A2, A3, A4, JORDAN3: 31;

          hence ex i1 be Nat st 1 <= i1 & (i1 + 1) <= ( len ( L_Cut (f,p))) & q in ( LSeg (( L_Cut (f,p)),i1)) by SPPOL_2: 13;

        end;

      end;

      then

       A22: q in ( L~ ( L_Cut (f,p))) by SPPOL_2: 17;

      then

       A23: ( Index (q,( L_Cut (f,p)))) < ( len ( L_Cut (f,p))) by JORDAN3: 8;

      1 <= ( Index (q,( L_Cut (f,p)))) by A22, JORDAN3: 8;

      then 1 <= ( len ( L_Cut (f,p))) by A23, XXREAL_0: 2;

      then p = (( L_Cut (f,p)) /. 1) by A21, FINSEQ_4: 15;

      hence thesis by A1, A2, A4, A5, A9, A11, A22, A21, Th42, JORDAN3: 32;

    end;

    theorem :: JORDAN23:43

    

     Th43: for f be non empty FinSequence of ( TOP-REAL 2) holds for p,q be Point of ( TOP-REAL 2) st f is almost-one-to-one special unfolded s.n.c. & ( len f) <> 2 & p in ( L~ f) & q in ( L~ f) & p <> q & p <> (f . 1) & q <> (f . 1) holds ( B_Cut (f,p,q)) is_S-Seq_joining (p,q)

    proof

      let f be non empty FinSequence of ( TOP-REAL 2);

      let p,q be Point of ( TOP-REAL 2);

      assume that

       A1: f is almost-one-to-one special unfolded s.n.c. and

       A2: ( len f) <> 2 and

       A3: p in ( L~ f) and

       A4: q in ( L~ f) and

       A5: p <> q and

       A6: p <> (f . 1) and

       A7: q <> (f . 1);

      per cases ;

        suppose ( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

        hence thesis by A1, A3, A4, A5, A6, Lm1;

      end;

        suppose

         A8: not (( Index (p,f)) < ( Index (q,f)) or ( Index (p,f)) = ( Index (q,f)) & LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))));

         A9:

        now

          assume that

           A10: ( Index (p,f)) = ( Index (q,f)) and

           A11: not LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)));

          

           A12: ( Index (p,f)) < ( len f) by A3, JORDAN3: 8;

          

           A13: 1 <= ( Index (p,f)) by A3, JORDAN3: 8;

          then

           A14: ( Index (p,f)) in ( dom f) by A12, FINSEQ_3: 25;

          f is weakly-one-to-one by A1, A2, Th7;

          then (f . ( Index (p,f))) <> (f . (( Index (p,f)) + 1)) by A13, A12;

          then

           A15: (f /. ( Index (p,f))) <> (f . (( Index (p,f)) + 1)) by A14, PARTFUN1:def 6;

          

           A16: (( Index (p,f)) + 1) <= ( len f) by A12, NAT_1: 13;

          then

           A17: ( LSeg (f,( Index (p,f)))) = ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A13, TOPREAL1:def 3;

          then

           A18: p in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A3, JORDAN3: 9;

          1 <= (( Index (p,f)) + 1) by NAT_1: 11;

          then (( Index (p,f)) + 1) in ( dom f) by A16, FINSEQ_3: 25;

          then

           A19: (f /. ( Index (p,f))) <> (f /. (( Index (p,f)) + 1)) by A15, PARTFUN1:def 6;

          q in ( LSeg ((f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1)))) by A4, A10, A17, JORDAN3: 9;

          then LT (q,p,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A11, A18, A19, JORDAN3: 28;

          hence LE (q,p,(f /. ( Index (q,f))),(f /. (( Index (q,f)) + 1))) by A10, JORDAN3:def 6;

        end;

        

         A20: ( Index (q,f)) < ( Index (p,f)) or ( Index (p,f)) = ( Index (q,f)) & not LE (p,q,(f /. ( Index (p,f))),(f /. (( Index (p,f)) + 1))) by A8, XXREAL_0: 1;

        ( B_Cut (f,p,q)) = ( Rev ( R_Cut (( L_Cut (f,q)),p))) by A8, JORDAN3:def 7;

        then

         A21: ( Rev ( B_Cut (f,q,p))) = ( B_Cut (f,p,q)) by A3, A4, A20, A9, JORDAN3:def 7;

        ( B_Cut (f,q,p)) is_S-Seq_joining (q,p) by A1, A3, A4, A5, A7, A20, A9, Lm1;

        hence thesis by A21, JORDAN3: 15;

      end;

    end;

    theorem :: JORDAN23:44

    for f be non empty FinSequence of ( TOP-REAL 2) holds for p,q be Point of ( TOP-REAL 2) st f is almost-one-to-one special unfolded s.n.c. & ( len f) <> 2 & p in ( L~ f) & q in ( L~ f) & p <> q & p <> (f . 1) & q <> (f . 1) holds ( B_Cut (f,p,q)) is being_S-Seq

    proof

      let f be non empty FinSequence of ( TOP-REAL 2);

      let p,q be Point of ( TOP-REAL 2);

      assume that

       A1: f is almost-one-to-one special unfolded s.n.c. and

       A2: ( len f) <> 2 and

       A3: p in ( L~ f) and

       A4: q in ( L~ f) and

       A5: p <> q and

       A6: p <> (f . 1) and

       A7: q <> (f . 1);

      ( B_Cut (f,p,q)) is_S-Seq_joining (p,q) by A1, A2, A3, A4, A5, A6, A7, Th43;

      hence thesis by JORDAN3:def 2;

    end;

    theorem :: JORDAN23:45

    for C be compact non vertical non horizontal Subset of ( TOP-REAL 2) holds for p,q be Point of ( TOP-REAL 2) st p in ( BDD ( L~ ( Cage (C,n)))) holds ex B be S-Sequence_in_R2 st B = ( B_Cut ((( Rotate (( Cage (C,n)),(( Cage (C,n)) /. ( Index (( South-Bound (p,( L~ ( Cage (C,n))))),( Cage (C,n))))))) | (( len ( Rotate (( Cage (C,n)),(( Cage (C,n)) /. ( Index (( South-Bound (p,( L~ ( Cage (C,n))))),( Cage (C,n)))))))) -' 1)),( South-Bound (p,( L~ ( Cage (C,n))))),( North-Bound (p,( L~ ( Cage (C,n))))))) & ex P be S-Sequence_in_R2 st P is_sequence_on ( GoB (B ^' <*( North-Bound (p,( L~ ( Cage (C,n))))), ( South-Bound (p,( L~ ( Cage (C,n)))))*>)) & ( L~ <*( North-Bound (p,( L~ ( Cage (C,n))))), ( South-Bound (p,( L~ ( Cage (C,n)))))*>) = ( L~ P) & (P /. 1) = ( North-Bound (p,( L~ ( Cage (C,n))))) & (P /. ( len P)) = ( South-Bound (p,( L~ ( Cage (C,n))))) & ( len P) >= 2 & ex B1 be S-Sequence_in_R2 st B1 is_sequence_on ( GoB (B ^' <*( North-Bound (p,( L~ ( Cage (C,n))))), ( South-Bound (p,( L~ ( Cage (C,n)))))*>)) & ( L~ B) = ( L~ B1) & (B /. 1) = (B1 /. 1) & (B /. ( len B)) = (B1 /. ( len B1)) & ( len B) <= ( len B1) & ex g be non constant standard special_circular_sequence st g = (B1 ^' P)

    proof

      let C be compact non vertical non horizontal Subset of ( TOP-REAL 2);

      let p,q be Point of ( TOP-REAL 2);

      set f = ( Cage (C,n));

      set Lf = ( L~ f);

      set a = ( North-Bound (p,Lf));

      set b = ( South-Bound (p,Lf));

      set Rotf = ( Rotate (f,(f /. ( Index (b,f)))));

      set rf = (Rotf | (( len Rotf) -' 1));

      

       A1: ( L~ Rotf) = ( L~ f) by REVROT_1: 33;

      

       A2: (( LSeg (Rotf,(( len Rotf) -' 1))) /\ ( LSeg (Rotf,1))) = {(Rotf /. 1)} by GOBOARD7: 34, REVROT_1: 30;

      then

       A3: ( LSeg (Rotf,(( len Rotf) -' 1))) meets ( LSeg (Rotf,1));

      

       A4: (Rotf /. 2) in ( LSeg ((Rotf /. 2),(Rotf /. 1))) by RLTOPSP1: 68;

      ( len Rotf) >= (1 + 1) by GOBOARD7: 34, XXREAL_0: 2;

      then

       A5: ( LSeg (Rotf,1)) = ( LSeg ((Rotf /. 1),(Rotf /. (1 + 1)))) by TOPREAL1:def 3;

      

       A6: (b `1 ) = (p `1 ) by JORDAN18: 16;

      ( len f) > 4 by GOBOARD7: 34;

      then

       A7: ((( len f) -' 1) + 1) = ( len f) by XREAL_1: 235, XXREAL_0: 2;

      then

       A8: (( len f) -' 1) < ( len f) by NAT_1: 13;

      set pion = <*a, b*>;

      

       A9: ( len f) > 1 by GOBOARD7: 34, XXREAL_0: 2;

      

       A10: (Rotf /. (( len Rotf) -' 1)) in ( LSeg ((Rotf /. (( len Rotf) -' 1)),(Rotf /. ( len Rotf)))) by RLTOPSP1: 68;

      assume that

       A11: p in ( BDD Lf);

      

       A12: a <> b by A11, JORDAN18: 20;

      

       A13: b in Lf by A11, JORDAN18: 17;

      then

       A14: ( Index (b,f)) < ( len f) by JORDAN3: 8;

      

       A15: for i be Nat st 1 <= i & i < ( Index (b,f)) holds (f /. i) <> (f /. ( Index (b,f))) by A14, GOBOARD7: 36;

      1 <= ( Index (b,f)) by A13, JORDAN3: 8;

      then

       A16: ( Index (b,f)) in ( dom f) by A14, FINSEQ_3: 25;

      then ((f /. ( Index (b,f))) .. f) <= ( Index (b,f)) by FINSEQ_5: 39;

      then ( 0 + ((f /. ( Index (b,f))) .. f)) < ( len f) by A14, XXREAL_0: 2;

      then

       A17: (( len f) - ((f /. ( Index (b,f))) .. f)) > (1 - 1) by XREAL_1: 20;

      

       A18: (f /. ( Index (b,f))) in ( rng f) by A16, PARTFUN2: 2;

      then ( len (f :- (f /. ( Index (b,f))))) = ((( len f) - ((f /. ( Index (b,f))) .. f)) + 1) by FINSEQ_5: 50;

      then 1 < ( len (f :- (f /. ( Index (b,f))))) by A17, XREAL_1: 19;

      

      then

       A19: ( LSeg (( Rotate (f,(f /. ( Index (b,f))))),1)) = ( LSeg (f,((1 -' 1) + ((f /. ( Index (b,f))) .. f)))) by A18, REVROT_1: 24

      .= ( LSeg (f,( 0 + ((f /. ( Index (b,f))) .. f)))) by XREAL_1: 232

      .= ( LSeg (f,( Index (b,f)))) by A16, A15, FINSEQ_6: 48;

      then

       A20: b in ( LSeg (( Rotate (f,(f /. ( Index (b,f))))),1)) by A13, JORDAN3: 9;

      

       A21: ( len f) > (1 + 1) by GOBOARD7: 34, XXREAL_0: 2;

      then

       A22: (( len f) - 1) > 1 by XREAL_1: 20;

      then

       A23: 1 < (( len f) -' 1) by XREAL_0:def 2;

      

       A24: ( len Rotf) = ( len f) by FINSEQ_6: 179;

      then

       A25: ( LSeg (Rotf,1)) = ( LSeg ((Rotf /. 1),(Rotf /. (1 + 1)))) by A21, TOPREAL1:def 3;

      

       A26: (a `1 ) = (p `1 ) by JORDAN18: 16;

      then ( LSeg (a,b)) is vertical by A6, SPPOL_1: 16;

      then

       A27: pion is being_S-Seq by A12, JORDAN1B: 7;

      

       A28: (p `2 ) < (a `2 ) by A11, JORDAN18: 18;

      

       A29: (b `2 ) < (p `2 ) by A11, JORDAN18: 18;

      then

       A30: p in ( LSeg (a,b)) by A26, A6, A28, GOBOARD7: 7;

      

       A31: ( LSeg (Rotf,(( len Rotf) -' 1))) = ( LSeg ((Rotf /. (( len Rotf) -' 1)),(Rotf /. ( len Rotf)))) by A24, A22, A7, TOPREAL1:def 3;

      reconsider rf as S-Sequence_in_R2 by A24, A22, A7, JORDAN4: 37;

      

       A32: ( L~ Rotf) = (( L~ rf) \/ ( LSeg (Rotf,(( len Rotf) -' 1)))) by A24, A22, A7, GOBOARD2: 3;

      

       A33: (Rotf /. 1) = (Rotf /. ( len Rotf)) by FINSEQ_6:def 1;

      

       A34: (b `2 ) < (a `2 ) by A29, A28, XXREAL_0: 2;

       A35:

      now

        assume

         A36: a in ( LSeg (Rotf,(( len Rotf) -' 1)));

        per cases by SPPOL_1: 19;

          suppose

           A37: ( LSeg (Rotf,1)) is vertical & ( LSeg (Rotf,(( len Rotf) -' 1))) is vertical;

          then

           A38: (b `1 ) = ((Rotf /. 1) `1 ) by A13, A19, A25, JORDAN3: 9, SPPOL_1: 41;

          

           A39: ((Rotf /. 1) `1 ) = ((Rotf /. (1 + 1)) `1 ) by A25, A37, SPPOL_1: 16;

          

           A40: ((Rotf /. (( len Rotf) -' 1)) `1 ) = ((Rotf /. ( len Rotf)) `1 ) by A31, A37, SPPOL_1: 16;

          per cases by A34, XXREAL_0: 2;

            suppose

             A41: (b `2 ) < ((Rotf /. 1) `2 );

            then

             A42: (((b `2 ) + ((Rotf /. 1) `2 )) / 2) < ((Rotf /. 1) `2 ) by XREAL_1: 226;

            

             A43: (b `2 ) < (((b `2 ) + ((Rotf /. 1) `2 )) / 2) by A41, XREAL_1: 226;

            set p1 = |[((Rotf /. 1) `1 ), (((b `2 ) + ((Rotf /. 1) `2 )) / 2)]|;

            

             A44: (p1 `1 ) = ((Rotf /. 1) `1 ) by EUCLID: 52;

            

             A45: (p1 `2 ) = (((b `2 ) + ((Rotf /. 1) `2 )) / 2) by EUCLID: 52;

            

             A46: ((Rotf /. 1) `2 ) > ((Rotf /. (1 + 1)) `2 ) by A20, A25, A41, TOPREAL1: 4;

            then ((Rotf /. (1 + 1)) `2 ) <= (b `2 ) by A20, A25, TOPREAL1: 4;

            then ((Rotf /. (1 + 1)) `2 ) < (p1 `2 ) by A45, A43, XXREAL_0: 2;

            then

             A47: p1 in Lf by A1, A5, A39, A44, A45, A42, GOBOARD7: 7, SPPOL_2: 17;

            ((Rotf /. ( len Rotf)) `2 ) <= ((Rotf /. (( len Rotf) -' 1)) `2 )

            proof

              

               A48: ((Rotf /. (( len Rotf) -' 1)) `2 ) < ((Rotf /. (1 + 1)) `2 ) or ((Rotf /. (( len Rotf) -' 1)) `2 ) >= ((Rotf /. (1 + 1)) `2 );

              assume ((Rotf /. ( len Rotf)) `2 ) > ((Rotf /. (( len Rotf) -' 1)) `2 );

              then (Rotf /. 2) in ( LSeg ((Rotf /. (( len Rotf) -' 1)),(Rotf /. ( len Rotf)))) or (Rotf /. (( len Rotf) -' 1)) in ( LSeg ((Rotf /. 2),(Rotf /. 1))) by A33, A39, A40, A46, A48, GOBOARD7: 7;

              then (Rotf /. 2) in {(Rotf /. 1)} or (Rotf /. (( len Rotf) -' 1)) in {(Rotf /. 1)} by A4, A10, A2, A25, A31, XBOOLE_0:def 4;

              then (Rotf /. (1 + 1)) = (Rotf /. 1) or (Rotf /. (( len Rotf) -' 1)) = (Rotf /. ( len Rotf)) by A33, TARSKI:def 1;

              hence contradiction by A24, A22, A9, A7, A8, Th5;

            end;

            then

             A49: ((Rotf /. ( len Rotf)) `2 ) <= (a `2 ) by A31, A36, TOPREAL1: 4;

            then (p1 `2 ) < (a `2 ) by A33, A45, A42, XXREAL_0: 2;

            then p1 in ( LSeg (b,a)) by A26, A6, A38, A44, A45, A43, GOBOARD7: 7;

            then p1 in (( LSeg (a,b)) /\ Lf) by A47, XBOOLE_0:def 4;

            then p1 in {a, b} by A11, JORDAN18: 22;

            hence contradiction by A33, A45, A43, A42, A49, TARSKI:def 2;

          end;

            suppose

             A50: ((Rotf /. 1) `2 ) < (a `2 );

            then

             A51: (((a `2 ) + ((Rotf /. 1) `2 )) / 2) < (a `2 ) by XREAL_1: 226;

            

             A52: ((Rotf /. 1) `2 ) < (((a `2 ) + ((Rotf /. 1) `2 )) / 2) by A50, XREAL_1: 226;

            set p1 = |[((Rotf /. 1) `1 ), (((a `2 ) + ((Rotf /. 1) `2 )) / 2)]|;

            

             A53: (p1 `1 ) = ((Rotf /. 1) `1 ) by EUCLID: 52;

            

             A54: (p1 `2 ) = (((a `2 ) + ((Rotf /. 1) `2 )) / 2) by EUCLID: 52;

            

             A55: ((Rotf /. (( len Rotf) -' 1)) `2 ) > ((Rotf /. ( len Rotf)) `2 ) by A33, A31, A36, A50, TOPREAL1: 4;

            then (a `2 ) <= ((Rotf /. (( len Rotf) -' 1)) `2 ) by A31, A36, TOPREAL1: 4;

            then (p1 `2 ) < ((Rotf /. (( len Rotf) -' 1)) `2 ) by A54, A51, XXREAL_0: 2;

            then

             A56: p1 in Lf by A1, A33, A31, A40, A53, A54, A52, GOBOARD7: 7, SPPOL_2: 17;

            ((Rotf /. (1 + 1)) `2 ) <= ((Rotf /. 1) `2 )

            proof

              

               A57: ((Rotf /. (( len Rotf) -' 1)) `2 ) < ((Rotf /. (1 + 1)) `2 ) or ((Rotf /. (( len Rotf) -' 1)) `2 ) >= ((Rotf /. (1 + 1)) `2 );

              assume ((Rotf /. (1 + 1)) `2 ) > ((Rotf /. 1) `2 );

              then (Rotf /. 2) in ( LSeg ((Rotf /. (( len Rotf) -' 1)),(Rotf /. ( len Rotf)))) or (Rotf /. (( len Rotf) -' 1)) in ( LSeg ((Rotf /. 2),(Rotf /. 1))) by A33, A39, A40, A55, A57, GOBOARD7: 7;

              then (Rotf /. 2) in {(Rotf /. 1)} or (Rotf /. (( len Rotf) -' 1)) in {(Rotf /. 1)} by A4, A10, A2, A25, A31, XBOOLE_0:def 4;

              then (Rotf /. (1 + 1)) = (Rotf /. 1) or (Rotf /. (( len Rotf) -' 1)) = (Rotf /. ( len Rotf)) by A33, TARSKI:def 1;

              hence contradiction by A24, A22, A9, A7, A8, Th5;

            end;

            then

             A58: (b `2 ) <= ((Rotf /. 1) `2 ) by A20, A25, TOPREAL1: 4;

            then (b `2 ) < (p1 `2 ) by A54, A52, XXREAL_0: 2;

            then p1 in ( LSeg (b,a)) by A26, A6, A38, A53, A54, A51, GOBOARD7: 7;

            then p1 in (( LSeg (a,b)) /\ Lf) by A56, XBOOLE_0:def 4;

            then p1 in {a, b} by A11, JORDAN18: 22;

            hence contradiction by A54, A52, A51, A58, TARSKI:def 2;

          end;

        end;

          suppose

           A59: ( LSeg (Rotf,1)) is vertical & ( LSeg (Rotf,(( len Rotf) -' 1))) is horizontal;

          then

           A60: (a `2 ) = ((Rotf /. ( len Rotf)) `2 ) by A31, A36, SPPOL_1: 40;

          (a `1 ) = ((Rotf /. ( len Rotf)) `1 ) by A26, A6, A13, A19, A33, A25, A59, JORDAN3: 9, SPPOL_1: 41;

          then a = (Rotf /. ( len Rotf)) by A60, TOPREAL3: 6;

          then a in ( LSeg ((Rotf /. 1),(Rotf /. 2))) by A33, RLTOPSP1: 68;

          then ( LSeg (a,b)) c= ( LSeg ((Rotf /. 1),(Rotf /. 2))) by A20, A25, TOPREAL1: 6;

          then p in Lf by A1, A30, A25, SPPOL_2: 17;

          then p in (( LSeg (a,b)) /\ Lf) by A30, XBOOLE_0:def 4;

          then p in {a, b} by A11, JORDAN18: 22;

          hence contradiction by A29, A28, TARSKI:def 2;

        end;

          suppose

           A61: ( LSeg (Rotf,1)) is horizontal & ( LSeg (Rotf,(( len Rotf) -' 1))) is vertical;

          then

           A62: (b `2 ) = ((Rotf /. 1) `2 ) by A13, A19, A25, JORDAN3: 9, SPPOL_1: 40;

          (b `1 ) = ((Rotf /. 1) `1 ) by A26, A6, A33, A31, A36, A61, SPPOL_1: 41;

          then b = (Rotf /. 1) by A62, TOPREAL3: 6;

          then b in ( LSeg ((Rotf /. (( len Rotf) -' 1)),(Rotf /. ( len Rotf)))) by A33, RLTOPSP1: 68;

          then ( LSeg (a,b)) c= ( LSeg ((Rotf /. (( len Rotf) -' 1)),(Rotf /. ( len Rotf)))) by A31, A36, TOPREAL1: 6;

          then p in Lf by A1, A30, A31, SPPOL_2: 17;

          then p in (( LSeg (a,b)) /\ Lf) by A30, XBOOLE_0:def 4;

          then p in {a, b} by A11, JORDAN18: 22;

          hence contradiction by A29, A28, TARSKI:def 2;

        end;

          suppose

           A63: ( LSeg (Rotf,1)) is horizontal & ( LSeg (Rotf,(( len Rotf) -' 1))) is horizontal;

          then

           A64: (a `2 ) = ((Rotf /. (( len Rotf) -' 1)) `2 ) by A31, A36, SPPOL_1: 40;

          (b `2 ) = ((Rotf /. 1) `2 ) by A13, A19, A25, A63, JORDAN3: 9, SPPOL_1: 40;

          hence contradiction by A29, A28, A3, A25, A31, A63, A64, SPRECT_3: 9;

        end;

      end;

      a in Lf by A11, JORDAN18: 17;

      then

       A65: a in ( L~ rf) by A1, A35, A32, XBOOLE_0:def 3;

      ( len rf) = (( len Rotf) -' 1) by FINSEQ_1: 59, NAT_D: 35;

      then (1 + 1) <= ( len rf) by A24, A23, NAT_1: 13;

      then

       A66: b in ( LSeg (rf,1)) by A20, SPPOL_2: 3;

      

       A67: ( LSeg (rf,1)) c= ( L~ rf) by TOPREAL3: 19;

      then

      reconsider BCut = ( B_Cut (rf,b,a)) as S-Sequence_in_R2 by A11, A66, A65, JORDAN18: 20, JORDAN3: 37;

      

       A68: (( len BCut) + 1) >= 1 by NAT_1: 11;

      set Ga = ( GoB (BCut ^' pion));

      now

        let n be Nat;

        assume

         A69: n in ( dom BCut);

        then

         A70: n <= ( len BCut) by FINSEQ_3: 25;

        ( dom BCut) c= ( dom (BCut ^' pion)) by Th23;

        then

        consider i,j be Nat such that

         A71: [i, j] in ( Indices ( GoB (BCut ^' pion))) and

         A72: ((BCut ^' pion) /. n) = (( GoB (BCut ^' pion)) * (i,j)) by A69, GOBOARD2: 14;

        take i, j;

        thus [i, j] in ( Indices Ga) by A71;

        1 <= n by A69, FINSEQ_3: 25;

        hence (BCut /. n) = (Ga * (i,j)) by A72, A70, FINSEQ_6: 159;

      end;

      then

      consider BCut1 be FinSequence of ( TOP-REAL 2) such that

       A73: BCut1 is_sequence_on Ga and

       A74: BCut1 is being_S-Seq and

       A75: ( L~ BCut) = ( L~ BCut1) and

       A76: (BCut /. 1) = (BCut1 /. 1) and

       A77: (BCut /. ( len BCut)) = (BCut1 /. ( len BCut1)) and

       A78: ( len BCut) <= ( len BCut1) by GOBOARD3: 2;

      reconsider BCut1 as S-Sequence_in_R2 by A74;

      

       A79: ( L~ BCut1) c= ( L~ rf) by A67, A66, A65, A75, JORDAN5B: 24;

      

       A80: ( len BCut1) in ( dom BCut1) by FINSEQ_5: 6;

      

       A81: 1 in ( dom BCut1) by FINSEQ_5: 6;

       A82:

      now

        assume BCut1 is constant;

        then (BCut1 /. 1) = (BCut1 /. ( len BCut1)) by A81, A80, FINSEQ_6:def 11;

        then (BCut1 /. ( len BCut1)) = b by A67, A66, A65, A76, Th19;

        hence contradiction by A11, A67, A66, A65, A77, Th20, JORDAN18: 20;

      end;

      (BCut /. ( len BCut)) = a by A67, A66, A65, Th20;

      then

       A83: a in ( LSeg ((BCut1 /. (( len BCut1) -' 1)),(BCut1 /. ( len BCut1)))) by A77, RLTOPSP1: 68;

      

       A84: ( len BCut1) >= (1 + 1) by TOPREAL1:def 8;

      then

       A85: (( len BCut1) - 1) >= 1 by XREAL_1: 19;

      take BCut;

      thus BCut = ( B_Cut ((( Rotate (( Cage (C,n)),(( Cage (C,n)) /. ( Index (( South-Bound (p,( L~ ( Cage (C,n))))),( Cage (C,n))))))) | (( len ( Rotate (( Cage (C,n)),(( Cage (C,n)) /. ( Index (( South-Bound (p,( L~ ( Cage (C,n))))),( Cage (C,n)))))))) -' 1)),( South-Bound (p,( L~ ( Cage (C,n))))),( North-Bound (p,( L~ ( Cage (C,n)))))));

      

       A86: (( LSeg (a,b)) /\ Lf) = {a, b} by A11, JORDAN18: 22;

      ( len BCut) > 0 by NAT_1: 3;

      then

       A87: ( len BCut) >= ( 0 + 1) by NAT_1: 13;

      

      then

       A88: ((BCut ^' pion) /. ( len BCut)) = (BCut /. ( len BCut)) by FINSEQ_6: 159

      .= a by A67, A66, A65, Th20

      .= (pion /. 1) by FINSEQ_4: 17;

      

       A89: ( len pion) = (1 + 1) by FINSEQ_1: 44;

      

      then

       A90: (( len (BCut ^' pion)) + 1) = (( len BCut) + (1 + 1)) by FINSEQ_6: 139

      .= ((( len BCut) + 1) + 1);

      then

       A91: ( len BCut) < ( len (BCut ^' pion)) by NAT_1: 13;

      now

        let n be Nat;

        assume n in ( dom pion);

        then

         A92: n in ( Seg 2) by FINSEQ_1: 89;

        per cases by A92, FINSEQ_1: 2, TARSKI:def 2;

          suppose

           A93: n = 1;

          ( len BCut) in ( Seg ( len (BCut ^' pion))) by A91, A87, FINSEQ_1: 1;

          then ( len BCut) in ( dom (BCut ^' pion)) by FINSEQ_1:def 3;

          then

          consider i,j be Nat such that

           A94: [i, j] in ( Indices Ga) and

           A95: ((BCut ^' pion) /. ( len BCut)) = (Ga * (i,j)) by GOBOARD2: 14;

          take i, j;

          thus [i, j] in ( Indices Ga) by A94;

          thus (pion /. n) = (Ga * (i,j)) by A88, A93, A95;

        end;

          suppose

           A96: n = (1 + 1);

          (( len BCut) + 1) in ( dom (BCut ^' pion)) by A90, A68, FINSEQ_3: 25;

          then

          consider i,j be Nat such that

           A97: [i, j] in ( Indices Ga) and

           A98: ((BCut ^' pion) /. (( len BCut) + 1)) = (Ga * (i,j)) by GOBOARD2: 14;

          take i, j;

          thus [i, j] in ( Indices Ga) by A97;

          thus (pion /. n) = (Ga * (i,j)) by A89, A96, A98, FINSEQ_6: 160;

        end;

      end;

      then

      consider pion1 be FinSequence of ( TOP-REAL 2) such that

       A99: pion1 is_sequence_on Ga and

       A100: pion1 is being_S-Seq and

       A101: ( L~ pion) = ( L~ pion1) and

       A102: (pion /. 1) = (pion1 /. 1) and

       A103: (pion /. ( len pion)) = (pion1 /. ( len pion1)) and

       A104: ( len pion) <= ( len pion1) by A27, GOBOARD3: 2;

      reconsider pion1 as S-Sequence_in_R2 by A100;

      

       A105: (pion1 /. ( len pion1)) = b by A89, A103, FINSEQ_4: 17

      .= (BCut1 /. 1) by A67, A66, A65, A76, Th19;

      

       A106: ( L~ rf) c= ( L~ f) by A1, TOPREAL3: 20;

      then ( L~ BCut1) c= Lf by A79;

      then (( L~ BCut1) /\ ( LSeg (a,b))) c= {a, b} by A86, XBOOLE_1: 26;

      then (( L~ BCut1) /\ ( L~ pion1)) c= {a, b} by A101, SPPOL_2: 21;

      then (( L~ BCut1) /\ ( L~ pion1)) c= {a, (BCut1 /. 1)} by A67, A66, A65, A76, Th19;

      then

       A107: (( L~ BCut1) /\ ( L~ pion1)) c= {(BCut1 /. 1), (pion1 /. 1)} by A102, FINSEQ_4: 17;

      ( len BCut1) > 1 by A84, NAT_1: 13;

      then

       A108: ((( len BCut1) -' 1) + 1) = ( len BCut1) by XREAL_1: 235;

      

       A109: (BCut1 /. ( len BCut1)) = a by A67, A66, A65, A77, Th20

      .= (pion1 /. 1) by A102, FINSEQ_4: 17;

      then

       A110: (BCut1 ^' pion1) is_sequence_on Ga by A99, A73, TOPREAL8: 12;

      

       A111: ( L~ BCut1) c= Lf by A106, A79;

       A112:

      now

        assume b in ( LSeg (BCut1,(( len BCut1) -' 1)));

        then b in ( LSeg ((BCut1 /. (( len BCut1) -' 1)),(BCut1 /. ( len BCut1)))) by A85, A108, TOPREAL1:def 3;

        then ( LSeg (a,b)) c= ( LSeg ((BCut1 /. (( len BCut1) -' 1)),(BCut1 /. ( len BCut1)))) by A83, TOPREAL1: 6;

        then p in ( LSeg ((BCut1 /. (( len BCut1) -' 1)),(BCut1 /. ( len BCut1)))) by A30;

        then p in ( LSeg (BCut1,(( len BCut1) -' 1))) by A85, A108, TOPREAL1:def 3;

        then p in ( L~ BCut1) by SPPOL_2: 17;

        then p in (( LSeg (a,b)) /\ Lf) by A30, A111, XBOOLE_0:def 4;

        then p in {a, b} by A11, JORDAN18: 22;

        hence contradiction by A29, A28, TARSKI:def 2;

      end;

      ( LSeg (BCut1,(( len BCut1) -' 1))) c= ( L~ BCut1) by TOPREAL3: 19;

      then ( LSeg (BCut1,(( len BCut1) -' 1))) c= ( L~ rf) by A79;

      then

       A113: ( LSeg (BCut1,(( len BCut1) -' 1))) c= Lf by A106;

      ( LSeg (pion1,1)) c= ( L~ pion) by A101, TOPREAL3: 19;

      then ( LSeg (pion1,1)) c= ( LSeg (a,b)) by SPPOL_2: 21;

      then (( LSeg (BCut1,(( len BCut1) -' 1))) /\ ( LSeg (pion1,1))) c= (( LSeg (a,b)) /\ Lf) by A113, XBOOLE_1: 27;

      then

       A114: (( LSeg (BCut1,(( len BCut1) -' 1))) /\ ( LSeg (pion1,1))) c= {a, b} by A11, JORDAN18: 22;

      

       A115: (( LSeg (BCut1,(( len BCut1) -' 1))) /\ ( LSeg (pion1,1))) = {(BCut1 /. ( len BCut1))}

      proof

        thus (( LSeg (BCut1,(( len BCut1) -' 1))) /\ ( LSeg (pion1,1))) c= {(BCut1 /. ( len BCut1))}

        proof

          let x be object;

          assume

           A116: x in (( LSeg (BCut1,(( len BCut1) -' 1))) /\ ( LSeg (pion1,1)));

          then x <> b by A112, XBOOLE_0:def 4;

          then x = a by A114, A116, TARSKI:def 2;

          then x = (BCut1 /. ( len BCut1)) by A67, A66, A65, A77, Th20;

          hence thesis by TARSKI:def 1;

        end;

        let x be object;

        assume x in {(BCut1 /. ( len BCut1))};

        then

         A117: x = (BCut1 /. ( len BCut1)) by TARSKI:def 1;

        then x in ( LSeg ((BCut1 /. (( len BCut1) -' 1)),(BCut1 /. ( len BCut1)))) by RLTOPSP1: 68;

        then

         A118: x in ( LSeg (BCut1,(( len BCut1) -' 1))) by A85, A108, TOPREAL1:def 3;

        x in ( LSeg ((pion1 /. 1),(pion1 /. (1 + 1)))) by A109, A117, RLTOPSP1: 68;

        then x in ( LSeg (pion1,1)) by A89, A104, TOPREAL1:def 3;

        hence thesis by A118, XBOOLE_0:def 4;

      end;

      take pion1;

      ( len <*a, b*>) = 2 by FINSEQ_1: 44;

      hence pion1 is_sequence_on ( GoB (BCut ^' <*( North-Bound (p,( L~ ( Cage (C,n))))), ( South-Bound (p,( L~ ( Cage (C,n)))))*>)) & ( L~ <*( North-Bound (p,( L~ ( Cage (C,n))))), ( South-Bound (p,( L~ ( Cage (C,n)))))*>) = ( L~ pion1) & (pion1 /. 1) = ( North-Bound (p,( L~ ( Cage (C,n))))) & (pion1 /. ( len pion1)) = ( South-Bound (p,( L~ ( Cage (C,n))))) & ( len pion1) >= 2 by A99, A101, A102, A103, A104, FINSEQ_4: 17;

      set g = (BCut1 ^' pion1);

      now

        assume ( len BCut) = 1;

        then (BCut /. 1) = a by A67, A66, A65, Th20;

        hence contradiction by A12, A67, A66, A65, Th19;

      end;

      then ( len BCut) > 1 by A87, XXREAL_0: 1;

      then ( len BCut1) > 1 by A78, XXREAL_0: 2;

      then

       A119: ( len BCut1) >= (1 + 1) by NAT_1: 13;

       {(BCut1 /. 1), (pion1 /. 1)} c= (( L~ BCut1) /\ ( L~ pion1))

      proof

        let x be object;

        assume x in {(BCut1 /. 1), (pion1 /. 1)};

        then

         A120: x = (BCut1 /. 1) or x = (pion1 /. 1) by TARSKI:def 2;

        then

         A121: x in ( L~ BCut1) by A109, A119, JORDAN3: 1;

        x in ( L~ pion1) by A89, A104, A105, A120, JORDAN3: 1;

        hence thesis by A121, XBOOLE_0:def 4;

      end;

      then (( L~ BCut1) /\ ( L~ pion1)) = {(BCut1 /. 1), (pion1 /. 1)} by A107;

      then

      reconsider g as non constant standard special_circular_sequence by A109, A82, A110, A115, A105, Th25, JORDAN8: 4, TOPREAL8: 11, TOPREAL8: 33, TOPREAL8: 34;

      take BCut1;

      thus BCut1 is_sequence_on ( GoB (BCut ^' <*( North-Bound (p,( L~ ( Cage (C,n))))), ( South-Bound (p,( L~ ( Cage (C,n)))))*>)) & ( L~ BCut) = ( L~ BCut1) & (BCut /. 1) = (BCut1 /. 1) & (BCut /. ( len BCut)) = (BCut1 /. ( len BCut1)) & ( len BCut) <= ( len BCut1) by A73, A75, A76, A77, A78;

      take g;

      thus thesis;

    end;