topreal8.miz



    begin

    theorem :: TOPREAL8:1

    

     Th1: for A,x,y be set st A c= {x, y} & x in A & not y in A holds A = {x}

    proof

      let A,x,y be set such that

       A1: A c= {x, y} and

       A2: x in A and

       A3: not y in A;

      per cases by A1, ZFMISC_1: 36;

        suppose A = {} ;

        hence thesis by A2;

      end;

        suppose A = {x};

        hence thesis;

      end;

        suppose A = {y};

        hence thesis by A3, TARSKI:def 1;

      end;

        suppose A = {x, y};

        hence thesis by A3, TARSKI:def 2;

      end;

    end;

    registration

      cluster trivial for Function;

      existence

      proof

        take {} ;

        thus thesis;

      end;

    end

    begin

    reserve G for Go-board,

i,j,k,m,n for Nat;

    registration

      cluster non constant for FinSequence;

      existence

      proof

        set f = the non constant FinSequence;

        take f;

        thus thesis;

      end;

    end

    theorem :: TOPREAL8:2

    

     Th2: for f be non trivial FinSequence holds 1 < ( len f)

    proof

      let f be non trivial FinSequence;

      (1 + 1) <= ( len f) by NAT_D: 60;

      hence thesis by NAT_1: 13;

    end;

    theorem :: TOPREAL8:3

    

     Th3: for D be non trivial set holds for f be non constant circular FinSequence of D holds ( len f) > 2

    proof

      let D be non trivial set;

      let f be non constant circular FinSequence of D;

      assume

       A1: ( len f) <= 2;

      per cases by A1, XXREAL_0: 1;

        suppose ( len f) < (1 + 1);

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

        then

        reconsider f as trivial Function by Th2;

        f is constant;

        hence contradiction;

      end;

        suppose

         A2: ( len f) = 2;

        then

         A3: ( dom f) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

        for n,m be Nat st n in ( dom f) & m in ( dom f) holds (f . n) = (f . m)

        proof

          let n,m be Nat such that

           A4: n in ( dom f) and

           A5: m in ( dom f);

          per cases by A3, A4, A5, TARSKI:def 2;

            suppose n = 1 & m = 1 or n = 2 & m = 2;

            hence thesis;

          end;

            suppose that

             A6: n = 1 and

             A7: m = 2;

            

             A8: m in ( dom f) by A3, A7, TARSKI:def 2;

            n in ( dom f) by A3, A6, TARSKI:def 2;

            

            hence (f . n) = (f /. 1) by A6, PARTFUN1:def 6

            .= (f /. ( len f)) by FINSEQ_6:def 1

            .= (f . m) by A2, A7, A8, PARTFUN1:def 6;

          end;

            suppose that

             A9: n = 2 and

             A10: m = 1;

            

             A11: n in ( dom f) by A3, A9, TARSKI:def 2;

            m in ( dom f) by A3, A10, TARSKI:def 2;

            

            hence (f . m) = (f /. 1) by A10, PARTFUN1:def 6

            .= (f /. ( len f)) by FINSEQ_6:def 1

            .= (f . n) by A2, A9, A11, PARTFUN1:def 6;

          end;

        end;

        hence contradiction by SEQM_3:def 10;

      end;

    end;

    theorem :: TOPREAL8:4

    

     Th4: for f be FinSequence, x be set holds x in ( rng f) or (x .. f) = 0

    proof

      let f be FinSequence, x be set;

      assume

       A1: not x in ( rng f);

       A2:

      now

        assume (f " {x}) <> {} ;

        then

        consider y be object such that

         A3: y in (f " {x}) by XBOOLE_0:def 1;

        (f . y) in {x} by A3, FUNCT_1:def 7;

        then

         A4: (f . y) = x by TARSKI:def 1;

        y in ( dom f) by A3, FUNCT_1:def 7;

        hence contradiction by A1, A4, FUNCT_1: 3;

      end;

      

      thus (x .. f) = (( Sgm (f " {x})) . 1) by FINSEQ_4:def 4

      .= 0 by A2, FINSEQ_3: 43;

    end;

    theorem :: TOPREAL8:5

    

     Th5: for p be set, D be non empty set holds for f be non empty FinSequence of D holds for g be FinSequence of D st (p .. f) = ( len f) holds ((f ^ g) |-- p) = g

    proof

      let p be set, D be non empty set;

      let f be non empty FinSequence of D;

      let g be FinSequence of D such that

       A1: (p .. f) = ( len f);

      

       A2: p in ( rng f) by A1, Th4;

      then

       A3: (p .. (f ^ g)) = ( len f) by A1, FINSEQ_6: 6;

      ( rng f) c= ( rng (f ^ g)) by FINSEQ_1: 29;

      

      hence ((f ^ g) |-- p) = ((f ^ g) /^ (p .. (f ^ g))) by A2, FINSEQ_5: 35

      .= g by A3;

    end;

    theorem :: TOPREAL8:6

    

     Th6: for D be non empty set holds for f be non empty one-to-one FinSequence of D holds ((f /. ( len f)) .. f) = ( len f)

    proof

      let D be non empty set;

      let f be non empty one-to-one FinSequence of D;

      

       A1: ( len f) in ( dom f) by FINSEQ_5: 6;

      

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

      proof

        let i be Nat such that

         A3: 1 <= i and

         A4: i < ( len f);

        i in ( dom f) by A3, A4, FINSEQ_3: 25;

        hence thesis by A1, A4, FUNCT_1:def 4;

      end;

      (f /. ( len f)) = (f . ( len f)) by A1, PARTFUN1:def 6;

      hence thesis by A1, A2, FINSEQ_6: 2;

    end;

    theorem :: TOPREAL8:7

    

     Th7: for f,g be FinSequence holds ( len f) <= ( len (f ^' g))

    proof

      let f,g be FinSequence;

      (f ^' g) = (f ^ ((2,( len g)) -cut g)) by FINSEQ_6:def 5;

      then ( len (f ^' g)) = (( len f) + ( len ((2,( len g)) -cut g))) by FINSEQ_1: 22;

      hence thesis by NAT_1: 11;

    end;

    theorem :: TOPREAL8:8

    

     Th8: for f,g be FinSequence holds for x be set st x in ( rng f) holds (x .. f) = (x .. (f ^' g))

    proof

      let f,g be FinSequence, x be set;

      assume

       A1: x in ( rng f);

      then

       A2: (f . (x .. f)) = x by FINSEQ_4: 19;

      

       A3: (x .. f) in ( dom f) by A1, FINSEQ_4: 20;

      then

       A4: (x .. f) <= ( len f) by FINSEQ_3: 25;

      

       A5: for i be Nat st 1 <= i & i < (x .. f) holds ((f ^' g) . i) <> x

      proof

        let i be Nat such that

         A6: 1 <= i and

         A7: i < (x .. f);

        

         A8: i < ( len f) by A4, A7, XXREAL_0: 2;

        then

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

        ((f ^' g) . i) = (f . i) by A6, A8, FINSEQ_6: 140;

        hence thesis by A7, A9, FINSEQ_4: 24;

      end;

      ( len f) <= ( len (f ^' g)) by Th7;

      then

       A10: ( dom f) c= ( dom (f ^' g)) by FINSEQ_3: 30;

      1 <= (x .. f) by A3, FINSEQ_3: 25;

      then ((f ^' g) . (x .. f)) = x by A2, A4, FINSEQ_6: 140;

      hence thesis by A3, A10, A5, FINSEQ_6: 2;

    end;

    theorem :: TOPREAL8:9

    for f be non empty FinSequence holds for g be FinSequence holds ( len g) <= ( len (f ^' g))

    proof

      let f be non empty FinSequence, g be FinSequence;

      per cases ;

        suppose g = {} ;

        hence thesis;

      end;

        suppose

         A1: g <> {} ;

        

         A2: ( len f) >= 1 by NAT_1: 14;

        (( len (f ^' g)) + 1) = (( len f) + ( len g)) by A1, FINSEQ_6: 139;

        then (( len (f ^' g)) + 1) >= (1 + ( len g)) by A2, XREAL_1: 6;

        hence thesis by XREAL_1: 6;

      end;

    end;

    theorem :: TOPREAL8:10

    

     Th10: for f,g be FinSequence holds ( rng f) c= ( rng (f ^' g))

    proof

      let f,g be FinSequence;

      (f ^' g) = (f ^ ((2,( len g)) -cut g)) by FINSEQ_6:def 5;

      hence thesis by FINSEQ_1: 29;

    end;

    theorem :: TOPREAL8:11

    

     Th11: for D be non empty set holds for f be non empty FinSequence of D holds for g be non trivial FinSequence of D st (g /. ( len g)) = (f /. 1) holds (f ^' g) is circular

    proof

      let D be non empty set;

      let f be non empty FinSequence of D, g be non trivial FinSequence of D;

      assume (g /. ( len g)) = (f /. 1);

      

      hence ((f ^' g) /. 1) = (g /. ( len g)) by FINSEQ_6: 155

      .= ((f ^' g) /. ( len (f ^' g))) by FINSEQ_6: 156;

    end;

    theorem :: TOPREAL8:12

    

     Th12: for D be non empty set holds for M be Matrix of D holds for f be FinSequence of D holds for g be non empty FinSequence of D st (f /. ( len f)) = (g /. 1) & f is_sequence_on M & g is_sequence_on M holds (f ^' g) is_sequence_on M

    proof

      let D be non empty set;

      let M be Matrix of D;

      let f be FinSequence of D;

      let g be non empty FinSequence of D such that

       A1: (f /. ( len f)) = (g /. 1) and

       A2: f is_sequence_on M and

       A3: g is_sequence_on M;

      

       A4: (( len (f ^' g)) + 1) = (( len f) + ( len g)) by FINSEQ_6: 139;

      thus for n st n in ( dom (f ^' g)) holds ex i, j st [i, j] in ( Indices M) & ((f ^' g) /. n) = (M * (i,j))

      proof

        let n such that

         A5: n in ( dom (f ^' g));

        per cases ;

          suppose

           A6: n <= ( len f);

          

           A7: 1 <= n by A5, FINSEQ_3: 25;

          then n in ( dom f) by A6, FINSEQ_3: 25;

          then

          consider i, j such that

           A8: [i, j] in ( Indices M) and

           A9: (f /. n) = (M * (i,j)) by A2;

          take i, j;

          thus [i, j] in ( Indices M) by A8;

          thus thesis by A6, A7, A9, FINSEQ_6: 159;

        end;

          suppose

           A10: n > ( len f);

          then

          consider k be Nat such that

           A11: n = (( len f) + k) by NAT_1: 10;

          reconsider k as Nat;

          

           A12: 1 <= (k + 1) by NAT_1: 11;

          n <= ( len (f ^' g)) by A5, FINSEQ_3: 25;

          then n < (( len f) + ( len g)) by A4, NAT_1: 13;

          then

           A13: k < ( len g) by A11, XREAL_1: 6;

          then (k + 1) <= ( len g) by NAT_1: 13;

          then (k + 1) in ( dom g) by A12, FINSEQ_3: 25;

          then

          consider i, j such that

           A14: [i, j] in ( Indices M) and

           A15: (g /. (k + 1)) = (M * (i,j)) by A3;

          take i, j;

          thus [i, j] in ( Indices M) by A14;

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

          then 1 <= k by A11, XREAL_1: 6;

          hence thesis by A11, A13, A15, FINSEQ_6: 160;

        end;

      end;

      let n such that

       A16: n in ( dom (f ^' g)) and

       A17: (n + 1) in ( dom (f ^' g));

      let m, k, i, j such that

       A18: [m, k] in ( Indices M) and

       A19: [i, j] in ( Indices M) and

       A20: ((f ^' g) /. n) = (M * (m,k)) and

       A21: ((f ^' g) /. (n + 1)) = (M * (i,j));

      per cases by XXREAL_0: 1;

        suppose

         A22: n < ( len f);

        then

         A23: (n + 1) <= ( len f) by NAT_1: 13;

        then

         A24: (f /. (n + 1)) = (M * (i,j)) by A21, FINSEQ_6: 159, NAT_1: 11;

        

         A25: 1 <= n by A16, FINSEQ_3: 25;

        then

         A26: n in ( dom f) by A22, FINSEQ_3: 25;

        1 <= (n + 1) by NAT_1: 11;

        then

         A27: (n + 1) in ( dom f) by A23, FINSEQ_3: 25;

        (f /. n) = (M * (m,k)) by A20, A22, A25, FINSEQ_6: 159;

        hence thesis by A2, A18, A19, A26, A27, A24;

      end;

        suppose

         A28: n > ( len f);

        then

        consider k0 be Nat such that

         A29: n = (( len f) + k0) by NAT_1: 10;

        reconsider k0 as Nat;

        

         A30: 1 <= (k0 + 1) by NAT_1: 11;

        n <= ( len (f ^' g)) by A16, FINSEQ_3: 25;

        then n < (( len f) + ( len g)) by A4, NAT_1: 13;

        then

         A31: k0 < ( len g) by A29, XREAL_1: 6;

        then (k0 + 1) <= ( len g) by NAT_1: 13;

        then

         A32: (k0 + 1) in ( dom g) by A30, FINSEQ_3: 25;

        

         A33: 1 <= ((k0 + 1) + 1) by NAT_1: 11;

        (n + 1) <= ( len (f ^' g)) by A17, FINSEQ_3: 25;

        then (( len f) + (k0 + 1)) < (( len f) + ( len g)) by A4, A29, NAT_1: 13;

        then

         A34: (k0 + 1) < ( len g) by XREAL_1: 6;

        then ((k0 + 1) + 1) <= ( len g) by NAT_1: 13;

        then

         A35: ((k0 + 1) + 1) in ( dom g) by A33, FINSEQ_3: 25;

        (( len f) + 1) <= n by A28, NAT_1: 13;

        then 1 <= k0 by A29, XREAL_1: 6;

        then

         A36: (g /. (k0 + 1)) = (M * (m,k)) by A20, A29, A31, FINSEQ_6: 160;

        (g /. ((k0 + 1) + 1)) = ((f ^' g) /. (( len f) + (k0 + 1))) by A34, FINSEQ_6: 160, NAT_1: 11

        .= (M * (i,j)) by A21, A29;

        hence thesis by A3, A18, A19, A32, A35, A36;

      end;

        suppose

         A37: n = ( len f);

        (n + 1) <= ( len (f ^' g)) by A17, FINSEQ_3: 25;

        then (( len f) + 1) < (( len f) + ( len g)) by A4, A37, NAT_1: 13;

        then

         A38: 1 < ( len g) by XREAL_1: 6;

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

        then

         A39: (1 + 1) in ( dom g) by FINSEQ_3: 25;

        1 <= n by A16, FINSEQ_3: 25;

        then

         A40: (g /. 1) = (M * (m,k)) by A1, A20, A37, FINSEQ_6: 159;

        

         A41: 1 in ( dom g) by FINSEQ_5: 6;

        (g /. (1 + 1)) = (M * (i,j)) by A21, A37, A38, FINSEQ_6: 160;

        hence thesis by A3, A18, A19, A40, A39, A41;

      end;

    end;

    

     Lm1: for p be FinSequence, m,n be Nat st 1 <= m & m <= (n + 1) & n <= ( len p) holds (( len ((m,n) -cut p)) + m) = (n + 1) & for i be Nat st i < ( len ((m,n) -cut p)) holds (((m,n) -cut p) . (i + 1)) = (p . (m + i))

    proof

      let p be FinSequence, m,n be Nat such that

       A1: 1 <= m and

       A2: m <= (n + 1) and

       A3: n <= ( len p);

      

       A4: m = (n + 1) or m < (n + 1) by A2, XXREAL_0: 1;

      per cases by A4, NAT_1: 13;

        suppose

         A5: m = (n + 1);

        then n < m by XREAL_1: 29;

        then ((m,n) -cut p) = {} by FINSEQ_6:def 4;

        hence (( len ((m,n) -cut p)) + m) = (n + 1) by A5;

         not (1 <= m & m <= n & n <= ( len p)) by A5, XREAL_1: 29;

        hence thesis by CARD_1: 27, FINSEQ_6:def 4;

      end;

        suppose m <= n;

        hence thesis by A1, A3, FINSEQ_6:def 4;

      end;

    end;

    theorem :: TOPREAL8:13

    

     Th13: for D be set, f be FinSequence of D st 1 <= k holds (((k + 1),( len f)) -cut f) = (f /^ k)

    proof

      let D be set, f be FinSequence of D such that

       A1: 1 <= k;

      per cases ;

        suppose

         A2: ( len f) < k;

        k <= (k + 1) by NAT_1: 11;

        then ( len f) < (k + 1) by A2, XXREAL_0: 2;

        

        hence (((k + 1),( len f)) -cut f) = {} by FINSEQ_6:def 4

        .= (f /^ k) by A2, FINSEQ_5: 32;

      end;

        suppose

         A3: f = {} ;

        then

         A4: ( len f) = 0 ;

        

        thus (((k + 1),( len f)) -cut f) = ( <*> D) by A3, FINSEQ_6:def 4

        .= (f /^ k) by A1, A4, RFINSEQ:def 1;

      end;

        suppose that

         A5: k <= ( len f);

        set IT = (((k + 1),( len f)) -cut f);

        

         A6: 1 <= (k + 1) by NAT_1: 11;

        

         A7: (k + 1) <= (( len f) + 1) by A5, XREAL_1: 6;

        

         A8: for m be Nat st m in ( dom IT) holds (IT . m) = (f . (m + k))

        proof

          let m be Nat such that

           A9: m in ( dom IT);

          1 <= m by A9, FINSEQ_3: 25;

          then

          consider i be Nat such that

           A10: m = (1 + i) by NAT_1: 10;

          reconsider i as Nat;

          m <= ( len IT) by A9, FINSEQ_3: 25;

          then i < ( len IT) by A10, NAT_1: 13;

          

          hence (IT . m) = (f . ((k + 1) + i)) by A6, A7, A10, Lm1

          .= (f . (m + k)) by A10;

        end;

        (( len f) + 1) = (( len IT) + (k + 1)) by A6, A7, Lm1

        .= ((( len IT) + k) + 1);

        then ( len IT) = (( len f) - k);

        hence thesis by A5, A8, RFINSEQ:def 1;

      end;

    end;

    theorem :: TOPREAL8:14

    

     Th14: for D be set, f be FinSequence of D st k <= ( len f) holds ((1,k) -cut f) = (f | k)

    proof

      let D be set, f be FinSequence of D such that

       A1: k <= ( len f);

      per cases ;

        suppose

         A2: ( 0 + 1) > k;

        

         A3: (f | 0 ) = {} ;

        k = 0 by A2, NAT_1: 13;

        hence thesis by A3, FINSEQ_6:def 4;

      end;

        suppose

         A4: 1 <= k;

        

         A5: (( len (f | k)) + 1) = (k + 1) by A1, FINSEQ_1: 59;

        for i be Nat st i < ( len (f | k)) holds ((f | k) . (i + 1)) = (f . (1 + i))

        proof

          let i be Nat;

          assume i < ( len (f | k));

          then (i + 1) <= k by A5, NAT_1: 13;

          hence thesis by FINSEQ_3: 112;

        end;

        hence thesis by A1, A4, A5, FINSEQ_6:def 4;

      end;

    end;

    theorem :: TOPREAL8:15

    

     Th15: for p be set, D be non empty set holds for f be non empty FinSequence of D holds for g be FinSequence of D st (p .. f) = ( len f) holds ((f ^ g) -| p) = ((1,(( len f) -' 1)) -cut f)

    proof

      let p be set, D be non empty set, f be non empty FinSequence of D, g be FinSequence of D such that

       A1: (p .. f) = ( len f);

      p in ( rng f) by A1, Th4;

      then

       A2: (p .. (f ^ g)) = (p .. f) by FINSEQ_6: 6;

      reconsider i = (( len f) - 1) as Element of NAT by INT_1: 5, NAT_1: 14;

      

       A3: (( len f) -' 1) = i by NAT_1: 14, XREAL_1: 233;

      ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22;

      then

       A4: ( len f) <= ( len (f ^ g)) by NAT_1: 11;

      ( rng f) c= ( rng (f ^ g)) by FINSEQ_1: 29;

      

      hence ((f ^ g) -| p) = ((f ^ g) | ( Seg i)) by A1, A2, Th4, FINSEQ_4: 33

      .= ((f ^ g) | i) by FINSEQ_1:def 15

      .= ((1,(( len f) -' 1)) -cut (f ^ g)) by A4, A3, Th14, NAT_D: 44

      .= ((1,(( len f) -' 1)) -cut f) by MSSCYC_1: 2, NAT_D: 44;

    end;

    theorem :: TOPREAL8:16

    

     Th16: for D be non empty set holds for f,g be non empty FinSequence of D st ((g /. 1) .. f) = ( len f) holds ((f ^' g) :- (g /. 1)) = g

    proof

      let D be non empty set;

      let f,g be non empty FinSequence of D such that

       A1: ((g /. 1) .. f) = ( len f);

      

       A2: (g /. 1) in ( rng f) by A1, Th4;

      

       A3: 1 <= ( len g) by NAT_1: 14;

      

       A4: (f ^' g) = (f ^ ((2,( len g)) -cut g)) by FINSEQ_6:def 5;

      then ( rng f) c= ( rng (f ^' g)) by FINSEQ_1: 29;

      

      hence ((f ^' g) :- (g /. 1)) = ( <*(g /. 1)*> ^ ((f ^' g) |-- (g /. 1))) by A2, FINSEQ_6: 41

      .= ( <*(g /. 1)*> ^ ((2,( len g)) -cut g)) by A1, A4, Th5

      .= ( <*(g . 1)*> ^ ((2,( len g)) -cut g)) by A3, FINSEQ_4: 15

      .= (((1,1) -cut g) ^ (((1 + 1),( len g)) -cut g)) by A3, FINSEQ_6: 132

      .= g by FINSEQ_6: 135, NAT_1: 14;

    end;

    theorem :: TOPREAL8:17

    

     Th17: for D be non empty set holds for f,g be non empty FinSequence of D st ((g /. 1) .. f) = ( len f) holds ((f ^' g) -: (g /. 1)) = f

    proof

      let D be non empty set;

      let f,g be non empty FinSequence of D such that

       A1: ((g /. 1) .. f) = ( len f);

      

       A2: (g /. 1) in ( rng f) by A1, Th4;

      (g /. 1) in ( rng f) by A1, Th4;

      then

       A3: (g /. 1) = (f . ( len f)) by A1, FINSEQ_4: 19;

      

       A4: 1 <= ( len f) by NAT_1: 14;

      

       A5: ((( len f) -' 1) + 1) = ( len f) by NAT_1: 14, XREAL_1: 235;

      

       A6: (f ^' g) = (f ^ ((2,( len g)) -cut g)) by FINSEQ_6:def 5;

      then ( rng f) c= ( rng (f ^' g)) by FINSEQ_1: 29;

      

      hence ((f ^' g) -: (g /. 1)) = (((f ^' g) -| (g /. 1)) ^ <*(g /. 1)*>) by A2, FINSEQ_6: 40

      .= (((1,(( len f) -' 1)) -cut f) ^ <*(g /. 1)*>) by A1, A6, Th15

      .= (((1,(( len f) -' 1)) -cut f) ^ ((( len f),( len f)) -cut f)) by A4, A3, FINSEQ_6: 132

      .= f by A5, FINSEQ_6: 135, NAT_D: 44;

    end;

    theorem :: TOPREAL8:18

    

     Th18: for D be non trivial set holds for f be non empty FinSequence of D holds for g be non trivial FinSequence of D st (g /. 1) = (f /. ( len f)) & for i st 1 <= i & i < ( len f) holds (f /. i) <> (g /. 1) holds ( Rotate ((f ^' g),(g /. 1))) = (g ^' f)

    proof

      let D be non trivial set;

      let f be non empty FinSequence of D;

      let g be non trivial FinSequence of D such that

       A1: (g /. 1) = (f /. ( len f)) and

       A2: for i st 1 <= i & i < ( len f) holds (f /. i) <> (g /. 1);

      

       A3: (g /. 1) in ( rng f) by A1, FINSEQ_6: 168;

      

       A4: ( len f) in ( dom f) by FINSEQ_5: 6;

      then

       A5: (f . ( len f)) = (f /. ( len f)) by PARTFUN1:def 6;

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

      proof

        let i be Nat such that

         A6: 1 <= i and

         A7: i < ( len f);

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

        hence thesis by A1, A2, A5, A6, A7;

      end;

      then

       A8: ((g /. 1) .. f) = ( len f) by A1, A4, A5, FINSEQ_6: 2;

      then

       A9: ((f ^' g) :- (g /. 1)) = g by Th16;

      ((f ^' g) -: (g /. 1)) = f by A8, Th17;

      then

       A10: (((f ^' g) -: (g /. 1)) /^ 1) = (((1 + 1),( len f)) -cut f) by Th13;

      ( rng f) c= ( rng (f ^' g)) by Th10;

      

      hence ( Rotate ((f ^' g),(g /. 1))) = (((f ^' g) :- (g /. 1)) ^ (((f ^' g) -: (g /. 1)) /^ 1)) by A3, FINSEQ_6:def 2

      .= (g ^' f) by A9, A10, FINSEQ_6:def 5;

    end;

    begin

    theorem :: TOPREAL8:19

    

     Th19: for f be non trivial FinSequence of ( TOP-REAL 2) holds ( LSeg (f,1)) = ( L~ (f | 2))

    proof

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

      

       A1: (1 + 1) <= ( len f) by NAT_D: 60;

      then

       A2: (f | 2) = <*(f /. 1), (f /. 2)*> by FINSEQ_5: 81;

      

      thus ( LSeg (f,1)) = ( LSeg ((f /. 1),(f /. (1 + 1)))) by A1, TOPREAL1:def 3

      .= ( L~ (f | 2)) by A2, SPPOL_2: 21;

    end;

    theorem :: TOPREAL8:20

    

     Th20: for f be s.c.c. FinSequence of ( TOP-REAL 2), n st n < ( len f) holds (f | n) is s.n.c.

    proof

      let f be s.c.c. FinSequence of ( TOP-REAL 2), n such that

       A1: n < ( len f);

      let i,j be Nat such that

       A2: (i + 1) < j;

      

       A3: ( len (f | n)) <= n by FINSEQ_5: 17;

      per cases ;

        suppose n < (j + 1);

        then ( len (f | n)) < (j + 1) by A3, XXREAL_0: 2;

        then ( LSeg ((f | n),j)) = {} by TOPREAL1:def 3;

        then (( LSeg ((f | n),i)) /\ ( LSeg ((f | n),j))) = {} ;

        hence thesis by XBOOLE_0:def 7;

      end;

        suppose ( len (f | n)) < (j + 1);

        then ( LSeg ((f | n),j)) = {} by TOPREAL1:def 3;

        then (( LSeg ((f | n),i)) /\ ( LSeg ((f | n),j))) = {} ;

        hence thesis by XBOOLE_0:def 7;

      end;

        suppose that

         A4: (j + 1) <= n and

         A5: (j + 1) <= ( len (f | n));

        (j + 1) < ( len f) by A1, A4, XXREAL_0: 2;

        then

         A6: ( LSeg (f,i)) misses ( LSeg (f,j)) by A2, GOBOARD5:def 4;

        j <= (j + 1) by NAT_1: 11;

        then

         A7: (i + 1) <= (j + 1) by A2, XXREAL_0: 2;

        ( LSeg (f,j)) = ( LSeg ((f | n),j)) by A5, SPPOL_2: 3;

        hence thesis by A5, A6, A7, SPPOL_2: 3, XXREAL_0: 2;

      end;

    end;

    theorem :: TOPREAL8:21

    

     Th21: for f be s.c.c. FinSequence of ( TOP-REAL 2), n st 1 <= n holds (f /^ n) is s.n.c.

    proof

      let f be s.c.c. FinSequence of ( TOP-REAL 2), n such that

       A1: 1 <= n;

      let i,j be Nat such that

       A2: (i + 1) < j;

      per cases ;

        suppose i < 1;

        then ( LSeg ((f /^ n),i)) = {} by TOPREAL1:def 3;

        then (( LSeg ((f /^ n),i)) /\ ( LSeg ((f /^ n),j))) = {} ;

        hence thesis by XBOOLE_0:def 7;

      end;

        suppose n > ( len f);

        then (f /^ n) = ( <*> the carrier of ( TOP-REAL 2)) by RFINSEQ:def 1;

        then not (1 <= i & (i + 1) <= ( len (f /^ n)));

        then ( LSeg ((f /^ n),i)) = {} by TOPREAL1:def 3;

        then (( LSeg ((f /^ n),i)) /\ ( LSeg ((f /^ n),j))) = {} ;

        hence thesis by XBOOLE_0:def 7;

      end;

        suppose ( len (f /^ n)) <= j;

        then ( len (f /^ n)) < (j + 1) by NAT_1: 13;

        then ( LSeg ((f /^ n),j)) = {} by TOPREAL1:def 3;

        then (( LSeg ((f /^ n),i)) /\ ( LSeg ((f /^ n),j))) = {} ;

        hence thesis by XBOOLE_0:def 7;

      end;

        suppose that

         A3: n <= ( len f) and

         A4: 1 <= i and

         A5: j < ( len (f /^ n));

        

         A6: j < (( len f) - n) by A3, A5, RFINSEQ:def 1;

        then

         A7: (j + 1) <= (( len f) - n) by INT_1: 7;

        (1 + 1) <= (i + 1) by A4, XREAL_1: 6;

        then (1 + 1) <= j by A2, XXREAL_0: 2;

        then 1 < j by NAT_1: 13;

        then

         A8: ( LSeg (f,(j + n))) = ( LSeg ((f /^ n),j)) by A7, SPPOL_2: 5;

        ((i + 1) + n) < (j + n) by A2, XREAL_1: 6;

        then

         A9: ((i + n) + 1) < (j + n);

        j <= (j + 1) by NAT_1: 11;

        then (i + 1) <= (j + 1) by A2, XXREAL_0: 2;

        then

         A10: (i + 1) <= (( len f) - n) by A7, XXREAL_0: 2;

        (1 + 1) <= (i + n) by A1, A4, XREAL_1: 7;

        then

         A11: 1 < (i + n) by NAT_1: 13;

        (j + n) < ( len f) by A6, XREAL_1: 20;

        then ( LSeg (f,(i + n))) misses ( LSeg (f,(j + n))) by A11, A9, GOBOARD5:def 4;

        hence thesis by A4, A8, A10, SPPOL_2: 5;

      end;

    end;

    theorem :: TOPREAL8:22

    

     Th22: for f be circular s.c.c. FinSequence of ( TOP-REAL 2), n st n < ( len f) & ( len f) > 4 holds (f | n) is one-to-one

    proof

      let f be circular s.c.c. FinSequence of ( TOP-REAL 2), n such that

       A1: n < ( len f) and

       A2: ( len f) > 4;

      for c1,c2 be Element of NAT st c1 in ( dom (f | n)) & c2 in ( dom (f | n)) & ((f | n) /. c1) = ((f | n) /. c2) holds c1 = c2

      proof

        

         A3: ( len (f | n)) <= n by FINSEQ_5: 17;

        

         A4: ( len (f | n)) <= n by FINSEQ_5: 17;

        let c1,c2 be Element of NAT such that

         A5: c1 in ( dom (f | n)) and

         A6: c2 in ( dom (f | n)) and

         A7: ((f | n) /. c1) = ((f | n) /. c2);

        

         A8: 1 <= c1 by A5, FINSEQ_3: 25;

        c1 <= ( len (f | n)) by A5, FINSEQ_3: 25;

        then c1 <= n by A3, XXREAL_0: 2;

        then

         A9: c1 < ( len f) by A1, XXREAL_0: 2;

        

         A10: 1 <= c2 by A6, FINSEQ_3: 25;

        

         A11: ((f | n) /. c1) = (f /. c1) by A5, FINSEQ_4: 70;

        c2 <= ( len (f | n)) by A6, FINSEQ_3: 25;

        then c2 <= n by A4, XXREAL_0: 2;

        then

         A12: c2 < ( len f) by A1, XXREAL_0: 2;

        

         A13: ((f | n) /. c2) = (f /. c2) by A6, FINSEQ_4: 70;

        assume

         A14: c1 <> c2;

        per cases by A14, XXREAL_0: 1;

          suppose c1 < c2;

          hence thesis by A2, A7, A8, A12, A11, A13, GOBOARD7: 35;

        end;

          suppose c2 < c1;

          hence thesis by A2, A7, A10, A9, A11, A13, GOBOARD7: 35;

        end;

      end;

      hence thesis by PARTFUN2: 9;

    end;

    theorem :: TOPREAL8:23

    

     Th23: for f be circular s.c.c. FinSequence of ( TOP-REAL 2) st ( len f) > 4 holds for i,j be Nat st 1 < i & i < j & j <= ( len f) holds (f /. i) <> (f /. j)

    proof

      let f be circular s.c.c. FinSequence of ( TOP-REAL 2) such that

       A1: ( len f) > 4;

      let i,j be Nat such that

       A2: 1 < i and

       A3: i < j and

       A4: j <= ( len f);

      per cases by A4, XXREAL_0: 1;

        suppose j < ( len f);

        hence thesis by A1, A2, A3, GOBOARD7: 35;

      end;

        suppose j = ( len f);

        then

         A5: (f /. j) = (f /. 1) by FINSEQ_6:def 1;

        i < ( len f) by A3, A4, XXREAL_0: 2;

        hence thesis by A1, A2, A5, GOBOARD7: 35;

      end;

    end;

    theorem :: TOPREAL8:24

    

     Th24: for f be circular s.c.c. FinSequence of ( TOP-REAL 2), n st 1 <= n & ( len f) > 4 holds (f /^ n) is one-to-one

    proof

      let f be circular s.c.c. FinSequence of ( TOP-REAL 2), n such that

       A1: 1 <= n and

       A2: ( len f) > 4;

      for c1,c2 be Element of NAT st c1 in ( dom (f /^ n)) & c2 in ( dom (f /^ n)) & ((f /^ n) /. c1) = ((f /^ n) /. c2) holds c1 = c2

      proof

        let c1,c2 be Element of NAT such that

         A3: c1 in ( dom (f /^ n)) and

         A4: c2 in ( dom (f /^ n)) and

         A5: ((f /^ n) /. c1) = ((f /^ n) /. c2);

        

         A6: ((f /^ n) /. c1) = (f /. (c1 + n)) by A3, FINSEQ_5: 27;

        

         A7: n <= ( len f) by A3, RELAT_1: 38, RFINSEQ:def 1;

        then ( len (f /^ n)) = (( len f) - n) by RFINSEQ:def 1;

        then

         A8: (( len (f /^ n)) + n) = ( len f);

        ( len (f /^ n)) = (( len f) - n) by A7, RFINSEQ:def 1;

        then

         A9: (( len (f /^ n)) + n) = ( len f);

        c1 <= ( len (f /^ n)) by A3, FINSEQ_3: 25;

        then

         A10: (c1 + n) <= ( len f) by A9, XREAL_1: 6;

        ( 0 + 1) <= c1 by A3, FINSEQ_3: 25;

        then

         A11: (1 + 0 ) < (c1 + n) by A1, XREAL_1: 8;

        

         A12: ((f /^ n) /. c2) = (f /. (c2 + n)) by A4, FINSEQ_5: 27;

        c2 <= ( len (f /^ n)) by A4, FINSEQ_3: 25;

        then

         A13: (c2 + n) <= ( len f) by A8, XREAL_1: 6;

        ( 0 + 1) <= c2 by A4, FINSEQ_3: 25;

        then

         A14: (1 + 0 ) < (c2 + n) by A1, XREAL_1: 8;

        assume

         A15: c1 <> c2;

        per cases by A15, XXREAL_0: 1;

          suppose c1 < c2;

          then (c1 + n) < (c2 + n) by XREAL_1: 6;

          hence thesis by A2, A5, A11, A13, A6, A12, Th23;

        end;

          suppose c2 < c1;

          then (c2 + n) < (c1 + n) by XREAL_1: 6;

          hence thesis by A2, A5, A14, A10, A6, A12, Th23;

        end;

      end;

      hence thesis by PARTFUN2: 9;

    end;

    theorem :: TOPREAL8:25

    

     Th25: for f be special non empty FinSequence of ( TOP-REAL 2) holds ((m,n) -cut f) is special

    proof

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

      set h = ((m,n) -cut f);

      let i be Nat such that

       A1: 1 <= i and

       A2: (i + 1) <= ( len h);

      per cases ;

        suppose not (1 <= m & m <= n & n <= ( len f));

        then h = {} by FINSEQ_6:def 4;

        hence thesis by A2;

      end;

        suppose

         A3: 1 <= m & m <= n & n <= ( len f);

        then

         A4: (1 + 1) <= (i + m) by A1, XREAL_1: 7;

        then

         A5: 1 <= (i + m) by XXREAL_0: 2;

        

         A6: ((i -' 1) + m) = ((i + m) -' 1) by A1, NAT_D: 38;

        then

         A7: 1 <= ((i -' 1) + m) by A4, NAT_D: 55;

        

         A8: (((i -' 1) + m) + 1) = (((i + m) -' 1) + 1) by A1, NAT_D: 38

        .= (i + m) by A4, XREAL_1: 235, XXREAL_0: 2;

        

         A9: i < ( len h) by A2, NAT_1: 13;

        (( len h) + m) = (n + 1) by A3, FINSEQ_6:def 4;

        then (i + m) < (n + 1) by A9, XREAL_1: 6;

        then (i + m) <= n by NAT_1: 13;

        then

         A10: (i + m) <= ( len f) by A3, XXREAL_0: 2;

        then

         A11: ((i -' 1) + m) <= ( len f) by A6, NAT_D: 44;

        (i -' 1) <= i by NAT_D: 44;

        then

         A12: (i -' 1) < ( len h) by A9, XXREAL_0: 2;

        

         A13: (h /. (i + 1)) = (h . (i + 1)) by A2, FINSEQ_4: 15, NAT_1: 11

        .= (f . (i + m)) by A3, A9, FINSEQ_6:def 4

        .= (f /. (i + m)) by A5, A10, FINSEQ_4: 15;

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

        

        then (h /. i) = (h . ((i -' 1) + 1)) by A1, A9, FINSEQ_4: 15

        .= (f . ((i -' 1) + m)) by A3, A12, FINSEQ_6:def 4

        .= (f /. ((i -' 1) + m)) by A6, A4, A11, FINSEQ_4: 15, NAT_D: 55;

        hence thesis by A7, A10, A13, A8, TOPREAL1:def 5;

      end;

    end;

    theorem :: TOPREAL8:26

    

     Th26: for f be special non empty FinSequence of ( TOP-REAL 2) holds for g be special non trivial FinSequence of ( TOP-REAL 2) st (f /. ( len f)) = (g /. 1) holds (f ^' g) is special

    proof

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

      let g be special non trivial FinSequence of ( TOP-REAL 2) such that

       A1: (f /. ( len f)) = (g /. 1);

      set h = ((2,( len g)) -cut g);

      

       A2: (f ^' g) = (f ^ ((2,( len g)) -cut g)) by FINSEQ_6:def 5;

      

       A3: (1 + 1) <= ( len g) by NAT_D: 60;

      then

       A4: ((g /. 1) `1 ) = ((g /. (1 + 1)) `1 ) or ((g /. 1) `2 ) = ((g /. (1 + 1)) `2 ) by TOPREAL1:def 5;

      ( len g) <= (( len g) + 1) by NAT_1: 11;

      then

       A5: 2 <= (( len g) + 1) by A3, XXREAL_0: 2;

      ((( len h) + 1) + 1) = (( len h) + (1 + 1))

      .= (( len g) + 1) by A5, Lm1;

      then 1 <= ( len h) by A3, XREAL_1: 6;

      

      then

       A6: (h /. 1) = (h . 1) by FINSEQ_4: 15

      .= (g . (1 + 1)) by A3, FINSEQ_6: 138

      .= (g /. (1 + 1)) by A3, FINSEQ_4: 15;

      h is special by Th25;

      hence thesis by A1, A2, A6, A4, GOBOARD2: 8;

    end;

    theorem :: TOPREAL8:27

    

     Th27: for f be circular unfolded s.c.c. FinSequence of ( TOP-REAL 2) st ( len f) > 4 holds (( LSeg (f,1)) /\ ( L~ (f /^ 1))) = {(f /. 1), (f /. 2)}

    proof

      let f be circular unfolded s.c.c. FinSequence of ( TOP-REAL 2) such that

       A1: ( len f) > 4;

      

       A2: (1 + 2) <= ( len f) by A1, XXREAL_0: 2;

      set h2 = (f /^ 1);

      

       A3: 1 <= ( len f) by A1, XXREAL_0: 2;

      then

       A4: ( len h2) = (( len f) - 1) by RFINSEQ:def 1;

      then

       A5: (( len h2) + 1) = ( len f);

      ( len f) > (3 + 1) by A1;

      then

       A6: ( len h2) > (2 + 1) by A5, XREAL_1: 6;

      then

       A7: (1 + 1) <= ( len (f /^ 1)) by XXREAL_0: 2;

      set SFY = { ( LSeg ((f /^ 1),i)) : 1 < i & (i + 1) < ( len (f /^ 1)) }, Reszta = ( union SFY);

      

       A8: ((( len (f /^ 1)) -' 1) + 1) <= ( len (f /^ 1)) by A6, XREAL_1: 235, XXREAL_0: 2;

      

       A9: 1 < ( len f) by A1, XXREAL_0: 2;

      for Z be set holds Z in { {} } iff ex X,Y be set st X in {( LSeg (f,1))} & Y in SFY & Z = (X /\ Y)

      proof

        let Z be set;

        thus Z in { {} } implies ex X,Y be set st X in {( LSeg (f,1))} & Y in SFY & Z = (X /\ Y)

        proof

          assume

           A10: Z in { {} };

          take X = ( LSeg (f,1)), Y = ( LSeg (f,(2 + 1)));

          thus X in {( LSeg (f,1))} by TARSKI:def 1;

          Y = ( LSeg ((f /^ 1),2)) by A3, SPPOL_2: 4;

          hence Y in SFY by A6;

          

           A11: (1 + 1) < 3;

          (3 + 1) < ( len f) by A1;

          then X misses Y by A11, GOBOARD5:def 4;

          then (X /\ Y) = {} by XBOOLE_0:def 7;

          hence Z = (X /\ Y) by A10, TARSKI:def 1;

        end;

        given X,Y be set such that

         A12: X in {( LSeg (f,1))} and

         A13: Y in SFY and

         A14: Z = (X /\ Y);

        

         A15: X = ( LSeg (f,1)) by A12, TARSKI:def 1;

        consider i such that

         A16: Y = ( LSeg ((f /^ 1),i)) and

         A17: 1 < i and

         A18: (i + 1) < ( len (f /^ 1)) by A13;

        

         A19: (1 + 1) < (i + 1) by A17, XREAL_1: 6;

        

         A20: ((i + 1) + 1) < ( len f) by A5, A18, XREAL_1: 6;

        ( LSeg ((f /^ 1),i)) = ( LSeg (f,(i + 1))) by A9, A17, SPPOL_2: 4;

        then X misses Y by A15, A16, A20, A19, GOBOARD5:def 4;

        then Z = {} by A14, XBOOLE_0:def 7;

        hence thesis by TARSKI:def 1;

      end;

      then ( INTERSECTION ( {( LSeg (f,1))},SFY)) = { {} } by SETFAM_1:def 5;

      

      then

       A21: (( LSeg (f,1)) /\ Reszta) = ( union { {} }) by SETFAM_1: 25

      .= {} by ZFMISC_1: 25;

      

       A22: ( L~ (f /^ 1)) c= ((( LSeg ((f /^ 1),1)) \/ ( LSeg ((f /^ 1),(( len (f /^ 1)) -' 1)))) \/ Reszta)

      proof

        let u be object;

        assume u in ( L~ (f /^ 1));

        then

        consider e be set such that

         A23: u in e and

         A24: e in { ( LSeg ((f /^ 1),i)) : 1 <= i & (i + 1) <= ( len (f /^ 1)) } by TARSKI:def 4;

        consider i such that

         A25: e = ( LSeg ((f /^ 1),i)) and

         A26: 1 <= i and

         A27: (i + 1) <= ( len (f /^ 1)) by A24;

        per cases by A26, A27, XXREAL_0: 1;

          suppose i = 1;

          then u in (( LSeg ((f /^ 1),1)) \/ ( LSeg ((f /^ 1),(( len (f /^ 1)) -' 1)))) by A23, A25, XBOOLE_0:def 3;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose (i + 1) = ( len (f /^ 1));

          then i = (( len (f /^ 1)) -' 1) by NAT_D: 34;

          then u in (( LSeg ((f /^ 1),1)) \/ ( LSeg ((f /^ 1),(( len (f /^ 1)) -' 1)))) by A23, A25, XBOOLE_0:def 3;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose 1 < i & (i + 1) < ( len (f /^ 1));

          then e in SFY by A25;

          then u in Reszta by A23, TARSKI:def 4;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      

       A28: Reszta c= ( L~ (f /^ 1))

      proof

        let u be object;

        assume u in Reszta;

        then

        consider e be set such that

         A29: u in e and

         A30: e in SFY by TARSKI:def 4;

        ex i st e = ( LSeg ((f /^ 1),i)) & 1 < i & (i + 1) < ( len (f /^ 1)) by A30;

        then e in { ( LSeg ((f /^ 1),i)) : 1 <= i & (i + 1) <= ( len (f /^ 1)) };

        hence thesis by A29, TARSKI:def 4;

      end;

      (1 + (( len (f /^ 1)) -' 1)) = ( len (f /^ 1)) by A6, XREAL_1: 235, XXREAL_0: 2

      .= (( len f) -' 1) by A1, A4, XREAL_1: 233, XXREAL_0: 2;

      

      then

       A31: (( LSeg (f,1)) /\ ( LSeg ((f /^ 1),(( len (f /^ 1)) -' 1)))) = (( LSeg (f,1)) /\ ( LSeg (f,(( len f) -' 1)))) by A3, A7, NAT_D: 55, SPPOL_2: 4

      .= {(f /. 1)} by A1, REVROT_1: 30;

      (1 + 1) <= ( len h2) by A6, NAT_1: 13;

      then ( LSeg ((f /^ 1),1)) in { ( LSeg ((f /^ 1),i)) : 1 <= i & (i + 1) <= ( len (f /^ 1)) };

      then

       A32: ( LSeg ((f /^ 1),1)) c= ( L~ (f /^ 1)) by ZFMISC_1: 74;

      

       A33: (( LSeg (f,1)) /\ ( LSeg ((f /^ 1),1))) = (( LSeg (f,1)) /\ ( LSeg (f,(1 + 1)))) by A3, SPPOL_2: 4

      .= {(f /. (1 + 1))} by A2, TOPREAL1:def 6;

      1 <= (( len (f /^ 1)) -' 1) by A7, NAT_D: 55;

      then ( LSeg ((f /^ 1),(( len (f /^ 1)) -' 1))) in { ( LSeg ((f /^ 1),i)) : 1 <= i & (i + 1) <= ( len (f /^ 1)) } by A8;

      then ( LSeg ((f /^ 1),(( len (f /^ 1)) -' 1))) c= ( L~ (f /^ 1)) by ZFMISC_1: 74;

      then (( LSeg ((f /^ 1),1)) \/ ( LSeg ((f /^ 1),(( len (f /^ 1)) -' 1)))) c= ( L~ (f /^ 1)) by A32, XBOOLE_1: 8;

      then ((( LSeg ((f /^ 1),1)) \/ ( LSeg ((f /^ 1),(( len (f /^ 1)) -' 1)))) \/ Reszta) c= ( L~ (f /^ 1)) by A28, XBOOLE_1: 8;

      then ( L~ (f /^ 1)) = ((( LSeg ((f /^ 1),1)) \/ ( LSeg ((f /^ 1),(( len (f /^ 1)) -' 1)))) \/ Reszta) by A22, XBOOLE_0:def 10;

      

      hence (( LSeg (f,1)) /\ ( L~ (f /^ 1))) = ((( LSeg (f,1)) /\ (( LSeg ((f /^ 1),1)) \/ ( LSeg ((f /^ 1),(( len (f /^ 1)) -' 1))))) \/ {} ) by A21, XBOOLE_1: 23

      .= ( {(f /. 1)} \/ {(f /. 2)}) by A33, A31, XBOOLE_1: 23

      .= {(f /. 1), (f /. 2)} by ENUMSET1: 1;

    end;

    theorem :: TOPREAL8:28

    

     Th28: for f,g be FinSequence of ( TOP-REAL 2) st j < ( len f) holds ( LSeg ((f ^' g),j)) = ( LSeg (f,j))

    proof

      let f,g be FinSequence of ( TOP-REAL 2) such that

       A1: j < ( len f);

      per cases ;

        suppose

         A2: j < 1;

        

        hence ( LSeg ((f ^' g),j)) = {} by TOPREAL1:def 3

        .= ( LSeg (f,j)) by A2, TOPREAL1:def 3;

      end;

        suppose

         A3: 1 <= j;

        then

         A4: ((f ^' g) /. j) = (f /. j) by A1, FINSEQ_6: 159;

        

         A5: (j + 1) <= ( len f) by A1, NAT_1: 13;

        then

         A6: ((f ^' g) /. (j + 1)) = (f /. (j + 1)) by FINSEQ_6: 159, NAT_1: 11;

        ( len f) <= ( len (f ^' g)) by Th7;

        then (j + 1) <= ( len (f ^' g)) by A5, XXREAL_0: 2;

        

        hence ( LSeg ((f ^' g),j)) = ( LSeg (((f ^' g) /. j),((f ^' g) /. (j + 1)))) by A3, TOPREAL1:def 3

        .= ( LSeg (f,j)) by A3, A4, A5, A6, TOPREAL1:def 3;

      end;

    end;

    theorem :: TOPREAL8:29

    

     Th29: for f,g be non empty FinSequence of ( TOP-REAL 2) st 1 <= j & (j + 1) < ( len g) holds ( LSeg ((f ^' g),(( len f) + j))) = ( LSeg (g,(j + 1)))

    proof

      let f,g be non empty FinSequence of ( TOP-REAL 2) such that

       A1: 1 <= j and

       A2: (j + 1) < ( len g);

      

       A3: ((f ^' g) /. ((( len f) + j) + 1)) = ((f ^' g) /. (( len f) + (j + 1)))

      .= (g /. ((j + 1) + 1)) by A2, FINSEQ_6: 160, NAT_1: 11;

      (j + 0 ) <= (j + 1) by XREAL_1: 6;

      then j < ( len g) by A2, XXREAL_0: 2;

      then

       A4: ((f ^' g) /. (( len f) + j)) = (g /. (j + 1)) by A1, FINSEQ_6: 160;

      

       A5: 1 <= (j + 1) by NAT_1: 11;

      (( len f) + (j + 1)) < (( len f) + ( len g)) by A2, XREAL_1: 6;

      then ((( len f) + j) + 1) < (( len (f ^' g)) + 1) by FINSEQ_6: 139;

      then

       A6: ((( len f) + j) + 1) <= ( len (f ^' g)) by NAT_1: 13;

      

       A7: ((j + 1) + 1) <= ( len g) by A2, NAT_1: 13;

      j <= (( len f) + j) by NAT_1: 11;

      then 1 <= (( len f) + j) by A1, XXREAL_0: 2;

      

      hence ( LSeg ((f ^' g),(( len f) + j))) = ( LSeg (((f ^' g) /. (( len f) + j)),((f ^' g) /. ((( len f) + j) + 1)))) by A6, TOPREAL1:def 3

      .= ( LSeg (g,(j + 1))) by A4, A5, A3, A7, TOPREAL1:def 3;

    end;

    theorem :: TOPREAL8:30

    

     Th30: for f be non empty FinSequence of ( TOP-REAL 2) holds for g be non trivial FinSequence of ( TOP-REAL 2) st (f /. ( len f)) = (g /. 1) holds ( LSeg ((f ^' g),( len f))) = ( LSeg (g,1))

    proof

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

      

       A1: 1 <= ( len f) by NAT_1: 14;

      let g be non trivial FinSequence of ( TOP-REAL 2);

      assume (f /. ( len f)) = (g /. 1);

      then

       A2: ((f ^' g) /. (( len f) + 0 )) = (g /. ( 0 + 1)) by A1, FINSEQ_6: 159;

      

       A3: 1 < ( len g) by Th2;

      then

       A4: ((f ^' g) /. ((( len f) + 0 ) + 1)) = (g /. (( 0 + 1) + 1)) by FINSEQ_6: 160;

      

       A5: (1 + 1) <= ( len g) by A3, NAT_1: 13;

      ((( len f) + 0 ) + 1) < (( len f) + ( len g)) by A3, XREAL_1: 6;

      then ((( len f) + 0 ) + 1) < (( len (f ^' g)) + 1) by FINSEQ_6: 139;

      then ((( len f) + 0 ) + 1) <= ( len (f ^' g)) by NAT_1: 13;

      

      hence ( LSeg ((f ^' g),( len f))) = ( LSeg (((f ^' g) /. (( len f) + 0 )),((f ^' g) /. ((( len f) + 0 ) + 1)))) by A1, TOPREAL1:def 3

      .= ( LSeg (g,1)) by A2, A4, A5, TOPREAL1:def 3;

    end;

    theorem :: TOPREAL8:31

    

     Th31: for f be non empty FinSequence of ( TOP-REAL 2) holds for g be non trivial FinSequence of ( TOP-REAL 2) st (j + 1) < ( len g) & (f /. ( len f)) = (g /. 1) holds ( LSeg ((f ^' g),(( len f) + j))) = ( LSeg (g,(j + 1)))

    proof

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

      let g be non trivial FinSequence of ( TOP-REAL 2) such that

       A1: (j + 1) < ( len g) and

       A2: (f /. ( len f)) = (g /. 1);

      per cases by NAT_1: 14;

        suppose j = 0 ;

        hence thesis by A2, Th30;

      end;

        suppose 1 <= j;

        hence thesis by A1, Th29;

      end;

    end;

    theorem :: TOPREAL8:32

    

     Th32: for f be non empty s.n.c. unfolded FinSequence of ( TOP-REAL 2), i st 1 <= i & i < ( len f) holds (( LSeg (f,i)) /\ ( rng f)) = {(f /. i), (f /. (i + 1))}

    proof

      let f be non empty s.n.c. unfolded FinSequence of ( TOP-REAL 2), i such that

       A1: 1 <= i and

       A2: i < ( len f);

      

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

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

      then

       A4: (f /. i) in ( rng f) by A3, FUNCT_1: 3;

      assume

       A5: (( LSeg (f,i)) /\ ( rng f)) <> {(f /. i), (f /. (i + 1))};

      

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

      then (f /. i) in ( LSeg (f,i)) by A1, TOPREAL1: 21;

      then

       A7: (f /. i) in (( LSeg (f,i)) /\ ( rng f)) by A4, XBOOLE_0:def 4;

      

       A8: 1 < (i + 1) by A1, XREAL_1: 29;

      then

       A9: (i + 1) in ( dom f) by A6, FINSEQ_3: 25;

      then (f /. (i + 1)) = (f . (i + 1)) by PARTFUN1:def 6;

      then

       A10: (f /. (i + 1)) in ( rng f) by A9, FUNCT_1: 3;

      (f /. (i + 1)) in ( LSeg (f,i)) by A1, A6, TOPREAL1: 21;

      then (f /. (i + 1)) in (( LSeg (f,i)) /\ ( rng f)) by A10, XBOOLE_0:def 4;

      then {(f /. i), (f /. (i + 1))} c= (( LSeg (f,i)) /\ ( rng f)) by A7, ZFMISC_1: 32;

      then not (( LSeg (f,i)) /\ ( rng f)) c= {(f /. i), (f /. (i + 1))} by A5, XBOOLE_0:def 10;

      then

      consider x be object such that

       A11: x in (( LSeg (f,i)) /\ ( rng f)) and

       A12: not x in {(f /. i), (f /. (i + 1))};

      reconsider x as Point of ( TOP-REAL 2) by A11;

      

       A13: x in ( LSeg (f,i)) by A11, XBOOLE_0:def 4;

      x in ( rng f) by A11, XBOOLE_0:def 4;

      then

      consider j be object such that

       A14: j in ( dom f) and

       A15: x = (f . j) by FUNCT_1:def 3;

      

       A16: x = (f /. j) by A14, A15, PARTFUN1:def 6;

      reconsider j as Nat by A14;

      

       A17: 1 <= j by A14, FINSEQ_3: 25;

      reconsider j as Nat;

      

       A18: x <> (f /. i) by A12, TARSKI:def 2;

      then

       A19: j <> i by A14, A15, PARTFUN1:def 6;

      

       A20: x <> (f /. (i + 1)) by A12, TARSKI:def 2;

      then

       A21: j <> (i + 1) by A14, A15, PARTFUN1:def 6;

      now

        per cases by A19, XXREAL_0: 1;

          suppose

           A22: (j + 1) > ( len f);

          

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

          ( len f) <= j by A22, NAT_1: 13;

          then

           A24: j = ( len f) by A23, XXREAL_0: 1;

          consider k be Nat such that

           A25: ( len f) = (1 + k) by A6, A8, NAT_1: 10, XXREAL_0: 2;

          reconsider k as Nat;

          1 < ( len f) by A6, A8, XXREAL_0: 2;

          then 1 <= k by A25, NAT_1: 13;

          then

           A26: x in ( LSeg (f,k)) by A16, A24, A25, TOPREAL1: 21;

          i <= k by A2, A25, NAT_1: 13;

          then i < k by A20, A16, A24, A25, XXREAL_0: 1;

          then

           A27: (i + 1) <= k by NAT_1: 13;

          now

            per cases by A27, XXREAL_0: 1;

              suppose

               A28: (i + 1) = k;

              then (i + (1 + 1)) <= ( len f) by A25;

              then (( LSeg (f,i)) /\ ( LSeg (f,k))) = {(f /. (i + 1))} by A1, A28, TOPREAL1:def 6;

              then x in {(f /. (i + 1))} by A13, A26, XBOOLE_0:def 4;

              hence contradiction by A20, TARSKI:def 1;

            end;

              suppose (i + 1) < k;

              then ( LSeg (f,i)) misses ( LSeg (f,k)) by TOPREAL1:def 7;

              hence contradiction by A13, A26, XBOOLE_0: 3;

            end;

          end;

          hence contradiction;

        end;

          suppose that

           A29: i < j and

           A30: (j + 1) <= ( len f);

          (i + 1) <= j by A29, NAT_1: 13;

          then (i + 1) < j by A21, XXREAL_0: 1;

          then

           A31: ( LSeg (f,i)) misses ( LSeg (f,j)) by TOPREAL1:def 7;

          x in ( LSeg (f,j)) by A16, A17, A30, TOPREAL1: 21;

          hence contradiction by A13, A31, XBOOLE_0: 3;

        end;

          suppose

           A32: j < i;

          then (j + 1) <= (i + 1) by XREAL_1: 6;

          then (j + 1) <= ( len f) by A6, XXREAL_0: 2;

          then x in ( LSeg (f,j)) by A16, A17, TOPREAL1: 21;

          then

           A33: x in (( LSeg (f,i)) /\ ( LSeg (f,j))) by A13, XBOOLE_0:def 4;

          

           A34: (j + 1) <= i by A32, NAT_1: 13;

          now

            per cases by A34, XXREAL_0: 1;

              suppose

               A35: (j + 1) = i;

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

              then (j + (1 + 1)) <= ( len f);

              then (( LSeg (f,i)) /\ ( LSeg (f,j))) = {(f /. i)} by A17, A35, TOPREAL1:def 6;

              hence contradiction by A18, A33, TARSKI:def 1;

            end;

              suppose (j + 1) < i;

              then ( LSeg (f,j)) misses ( LSeg (f,i)) by TOPREAL1:def 7;

              hence contradiction by A33, XBOOLE_0: 4;

            end;

          end;

          hence contradiction;

        end;

      end;

      hence contradiction;

    end;

    

     Lm2: for f be non empty s.n.c. one-to-one unfolded FinSequence of ( TOP-REAL 2) holds for g be non trivial s.n.c. one-to-one unfolded FinSequence of ( TOP-REAL 2) holds for i, j st i < ( len f) & 1 < i holds for x be Point of ( TOP-REAL 2) st x in (( LSeg ((f ^' g),i)) /\ ( LSeg ((f ^' g),j))) holds x <> (f /. 1)

    proof

      let f be non empty s.n.c. one-to-one unfolded FinSequence of ( TOP-REAL 2);

      let g be non trivial s.n.c. one-to-one unfolded FinSequence of ( TOP-REAL 2);

      let i, j such that

       A1: i < ( len f) and

       A2: 1 < i;

      

       A3: 1 < (i + 1) by A2, XREAL_1: 29;

      

       A4: (( LSeg (f,i)) /\ ( rng f)) = {(f /. i), (f /. (i + 1))} by A1, A2, Th32;

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

      then

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

      

       A6: ( LSeg ((f ^' g),i)) = ( LSeg (f,i)) by A1, Th28;

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

      assume x in (( LSeg ((f ^' g),i)) /\ ( LSeg ((f ^' g),j)));

      then

       A7: x in ( LSeg (f,i)) by A6, XBOOLE_0:def 4;

      

       A8: 1 in ( dom f) by FINSEQ_5: 6;

      assume that

       A9: x = (f /. 1);

      x = (f . 1) by A9, A8, PARTFUN1:def 6;

      then x in ( rng f) by A8, FUNCT_1: 3;

      then x in (( LSeg (f,i)) /\ ( rng f)) by A7, XBOOLE_0:def 4;

      then

       A10: x = (f /. i) or x = (f /. (i + 1)) by A4, TARSKI:def 2;

      i in ( dom f) by A1, A2, FINSEQ_3: 25;

      hence contradiction by A2, A9, A8, A10, A3, A5, PARTFUN2: 10;

    end;

    

     Lm3: for f be non empty s.n.c. one-to-one unfolded FinSequence of ( TOP-REAL 2) holds for g be non trivial s.n.c. one-to-one unfolded FinSequence of ( TOP-REAL 2) holds for i, j st j > ( len f) & (j + 1) < ( len (f ^' g)) holds for x be Point of ( TOP-REAL 2) st x in (( LSeg ((f ^' g),i)) /\ ( LSeg ((f ^' g),j))) holds x <> (g /. ( len g))

    proof

      let f be non empty s.n.c. one-to-one unfolded FinSequence of ( TOP-REAL 2);

      let g be non trivial s.n.c. one-to-one unfolded FinSequence of ( TOP-REAL 2);

      let i, j such that

       A1: j > ( len f) and

       A2: (j + 1) < ( len (f ^' g));

      consider k be Nat such that

       A3: j = (( len f) + k) by A1, NAT_1: 10;

      (( len (f ^' g)) + 1) = (( len f) + ( len g)) by FINSEQ_6: 139;

      then

       A4: ((j + 1) + 1) < (( len f) + ( len g)) by A2, XREAL_1: 6;

      reconsider k as Nat;

      ((j + 1) + 1) = (( len f) + ((k + 1) + 1)) by A3;

      then

       A5: ((k + 1) + 1) < ( len g) by A4, XREAL_1: 6;

      1 <= ((k + 1) + 1) by NAT_1: 11;

      then

       A6: ((k + 1) + 1) in ( dom g) by A5, FINSEQ_3: 25;

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

       A7: x in (( LSeg ((f ^' g),i)) /\ ( LSeg ((f ^' g),j)));

      

       A8: ( len g) in ( dom g) by FINSEQ_5: 6;

      

       A9: (k + 1) <= ((k + 1) + 1) by NAT_1: 11;

      then

       A10: (k + 1) < ( len g) by A5, XXREAL_0: 2;

      then

       A11: (( LSeg (g,(k + 1))) /\ ( rng g)) = {(g /. (k + 1)), (g /. ((k + 1) + 1))} by Th32, NAT_1: 11;

      assume that

       A12: x = (g /. ( len g));

      x = (g . ( len g)) by A12, A8, PARTFUN1:def 6;

      then

       A13: x in ( rng g) by A8, FUNCT_1: 3;

      1 <= (k + 1) by NAT_1: 11;

      then

       A14: (k + 1) in ( dom g) by A10, FINSEQ_3: 25;

      (( len f) + 0 ) < (( len f) + k) by A1, A3;

      then 0 < k;

      then ( 0 + 1) <= k by NAT_1: 13;

      then ( LSeg ((f ^' g),j)) = ( LSeg (g,(k + 1))) by A3, A10, Th29;

      then x in ( LSeg (g,(k + 1))) by A7, XBOOLE_0:def 4;

      then x in (( LSeg (g,(k + 1))) /\ ( rng g)) by A13, XBOOLE_0:def 4;

      then x = (g /. (k + 1)) or x = (g /. ((k + 1) + 1)) by A11, TARSKI:def 2;

      hence contradiction by A12, A5, A9, A8, A14, A6, PARTFUN2: 10;

    end;

    theorem :: TOPREAL8:33

    

     Th33: for f,g be non trivial s.n.c. one-to-one unfolded FinSequence of ( TOP-REAL 2) st (( L~ f) /\ ( L~ g)) = {(f /. 1), (g /. 1)} & (f /. 1) = (g /. ( len g)) & (g /. 1) = (f /. ( len f)) holds (f ^' g) is s.c.c.

    proof

      let f,g be non trivial s.n.c. one-to-one unfolded FinSequence of ( TOP-REAL 2) such that

       A1: (( L~ f) /\ ( L~ g)) = {(f /. 1), (g /. 1)} and

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

       A3: (g /. 1) = (f /. ( len f));

      

       A4: for i st 1 <= i & i < ( len f) holds (f /. i) <> (g /. 1)

      proof

        

         A5: ( len f) in ( dom f) by FINSEQ_5: 6;

        then

         A6: (f /. ( len f)) = (f . ( len f)) by PARTFUN1:def 6;

        let i such that

         A7: 1 <= i and

         A8: i < ( len f);

        

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

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

        hence thesis by A3, A8, A9, A5, A6, FUNCT_1:def 4;

      end;

      

       A10: (( len (f ^' g)) + 1) = (( len f) + ( len g)) by FINSEQ_6: 139;

      

       A11: (( len (g ^' f)) + 1) = (( len f) + ( len g)) by FINSEQ_6: 139;

      let i, j such that

       A12: (i + 1) < j and

       A13: i > 1 & j < ( len (f ^' g)) or (j + 1) < ( len (f ^' g));

      

       A14: i < j by A12, NAT_1: 13;

      j <= (j + 1) by NAT_1: 11;

      then

       A15: j < ( len (f ^' g)) by A13, XXREAL_0: 2;

      per cases by NAT_1: 14;

        suppose i = 0 ;

        then ( LSeg ((f ^' g),i)) = {} by TOPREAL1:def 3;

        then (( LSeg ((f ^' g),i)) /\ ( LSeg ((f ^' g),j))) = {} ;

        hence thesis by XBOOLE_0:def 7;

      end;

        suppose

         A16: j < ( len f);

        then i < ( len f) by A14, XXREAL_0: 2;

        then

         A17: ( LSeg ((f ^' g),i)) = ( LSeg (f,i)) by Th28;

        ( LSeg ((f ^' g),j)) = ( LSeg (f,j)) by A16, Th28;

        hence thesis by A12, A17, TOPREAL1:def 7;

      end;

        suppose

         A18: i >= ( len f);

        then

        consider m be Nat such that

         A19: i = (( len f) + m) by NAT_1: 10;

        consider n be Nat such that

         A20: j = (( len f) + n) by A14, A18, NAT_1: 10, XXREAL_0: 2;

        reconsider m, n as Nat;

        

         A21: 1 <= (m + 1) by NAT_1: 11;

        (j + 1) < (( len f) + ( len g)) by A15, A10, XREAL_1: 6;

        then (( len f) + (n + 1)) < (( len f) + ( len g)) by A20;

        then

         A22: (n + 1) < ( len g) by XREAL_1: 6;

        

         A23: m < n by A14, A19, A20, XREAL_1: 6;

        then (m + 1) <= n by NAT_1: 13;

        then 1 <= n by A21, XXREAL_0: 2;

        then

         A24: ( LSeg ((f ^' g),j)) = ( LSeg (g,(n + 1))) by A20, A22, Th29;

        ((i + 1) + 1) < (j + 1) by A12, XREAL_1: 6;

        then (( len f) + (m + (1 + 1))) < (( len f) + (n + 1)) by A19, A20;

        then

         A25: ((m + 1) + 1) < (n + 1) by XREAL_1: 6;

        (m + 1) < (n + 1) by A23, XREAL_1: 6;

        then (m + 1) < ( len g) by A22, XXREAL_0: 2;

        then ( LSeg ((f ^' g),i)) = ( LSeg (g,(m + 1))) by A3, A19, Th31;

        hence thesis by A24, A25, TOPREAL1:def 7;

      end;

        suppose that

         A26: j >= ( len f) and

         A27: i < ( len f) and

         A28: 1 <= i;

        consider k be Nat such that

         A29: j = (( len f) + k) by A26, NAT_1: 10;

        reconsider k as Nat;

        (j + 1) < (( len f) + ( len g)) by A15, A10, XREAL_1: 6;

        then (( len f) + (k + 1)) < (( len f) + ( len g)) by A29;

        then (k + 1) < ( len g) by XREAL_1: 6;

        then ( LSeg ((f ^' g),j)) = ( LSeg (g,(k + 1))) by A3, A29, Th31;

        then

         A30: ( LSeg ((f ^' g),j)) c= ( L~ g) by TOPREAL3: 19;

        assume ( LSeg ((f ^' g),i)) meets ( LSeg ((f ^' g),j));

        then

        consider x be object such that

         A31: x in (( LSeg ((f ^' g),i)) /\ ( LSeg ((f ^' g),j))) by XBOOLE_0: 4;

        ( LSeg ((f ^' g),i)) = ( LSeg (f,i)) by A27, Th28;

        then ( LSeg ((f ^' g),i)) c= ( L~ f) by TOPREAL3: 19;

        then

         A32: (( LSeg ((f ^' g),i)) /\ ( LSeg ((f ^' g),j))) c= {(f /. 1), (g /. 1)} by A1, A30, XBOOLE_1: 27;

        now

          per cases by A13, A26, A31, A32, TARSKI:def 2, XXREAL_0: 1;

            suppose 1 < i & x = (f /. 1);

            hence contradiction by A27, A31, Lm2;

          end;

            suppose that

             A33: j > (( len f) + 0 ) and

             A34: x = (g /. 1);

            (j + 0 ) < (j + 1) by XREAL_1: 6;

            then

             A35: ( len f) < (j + 1) by A33, XXREAL_0: 2;

            (j + 1) < (( len (g ^' f)) + 1) by A15, A10, A11, XREAL_1: 6;

            then ((j + 1) -' ( len f)) < ( len g) by A11, A35, NAT_D: 54;

            then

             A36: ((j -' ( len f)) + 1) < ( len g) by A33, NAT_D: 38;

            

             A37: ( Rotate ((f ^' g),(g /. 1))) = (g ^' f) by A3, A4, Th18;

             0 < (j -' ( len f)) by A33, NAT_D: 52;

            then

             A38: ( 0 + 1) < ((j -' ( len f)) + 1) by XREAL_1: 6;

            

             A39: ( len f) in ( dom f) by FINSEQ_5: 6;

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

            then

             A40: (g /. 1) in ( rng f) by A3, A39, FUNCT_1: 3;

            

            then

             A41: ((g /. 1) .. (f ^' g)) = ((g /. 1) .. f) by Th8

            .= ( len f) by A3, Th6;

            

             A42: ( rng f) c= ( rng (f ^' g)) by Th10;

            then

             A43: ( LSeg ((f ^' g),j)) = ( LSeg (( Rotate ((f ^' g),(g /. 1))),((j -' ((g /. 1) .. (f ^' g))) + 1))) by A15, A33, A40, A41, REVROT_1: 25;

            (f ^' g) is circular by A2, Th11;

            then ( LSeg ((f ^' g),i)) = ( LSeg (( Rotate ((f ^' g),(g /. 1))),((i + ( len (f ^' g))) -' ((g /. 1) .. (f ^' g))))) by A27, A28, A40, A41, A42, REVROT_1: 32;

            hence contradiction by A31, A34, A37, A41, A43, A36, A38, Lm2;

          end;

            suppose that

             A44: j = ( len f) and

             A45: x = (g /. 1);

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

            then i < j by A12, XXREAL_0: 2;

            then ( LSeg ((f ^' g),i)) = ( LSeg (f,i)) by A44, Th28;

            then

             A46: (f /. ( len f)) in ( LSeg (f,i)) by A3, A31, A45, XBOOLE_0:def 4;

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

            then i < ( len f) by A12, A44, XXREAL_0: 2;

            then

             A47: i in ( dom f) by A28, FINSEQ_3: 25;

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

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

            hence contradiction by A12, A44, A47, A46, GOBOARD2: 2;

          end;

            suppose that

             A48: j > ( len f) and

             A49: x = (f /. 1) and

             A50: (j + 1) < ( len (f ^' g));

            thus thesis by A2, A31, A48, A49, A50, Lm3;

          end;

            suppose that

             A51: j = ( len f) and

             A52: x = (f /. 1) and

             A53: (j + 1) < ( len (f ^' g));

            ( 0 + 1) < ( len g) by Th2;

            then ( LSeg ((f ^' g),(( len f) + 0 ))) = ( LSeg (g,( 0 + 1))) by A3, Th31;

            then

             A54: (g /. ( len g)) in ( LSeg (g,1)) by A2, A31, A51, A52, XBOOLE_0:def 4;

            ((j + 1) + 1) < (( len f) + ( len g)) by A10, A53, XREAL_1: 6;

            then

             A55: (j + (1 + 1)) < (( len f) + ( len g));

            then (1 + 1) < ( len g) by A51, XREAL_1: 6;

            then

             A56: (1 + 1) in ( dom g) by FINSEQ_3: 25;

            1 in ( dom g) by FINSEQ_5: 6;

            hence contradiction by A51, A55, A54, A56, GOBOARD2: 2;

          end;

        end;

        hence contradiction;

      end;

    end;

    reserve f,g,g1,g2 for FinSequence of ( TOP-REAL 2);

    theorem :: TOPREAL8:34

    

     Th34: f is unfolded & g is unfolded & (f /. ( len f)) = (g /. 1) & (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (g,1))) = {(f /. ( len f))} implies (f ^' g) is unfolded

    proof

      assume that

       A1: f is unfolded and

       A2: g is unfolded and

       A3: (f /. ( len f)) = (g /. 1) and

       A4: (( LSeg (f,(( len f) -' 1))) /\ ( LSeg (g,1))) = {(f /. ( len f))};

      set c = (((1 + 1),( len g)) -cut g), k = (( len f) -' 1);

      reconsider g9 = g as unfolded FinSequence of ( TOP-REAL 2) by A2;

      

       A5: c = (g9 /^ 1) by Th13;

      

       A6: (f ^' g) = (f ^ (((1 + 1),( len g)) -cut g)) by FINSEQ_6:def 5;

      ( len g) <= 2 implies ( len g) = 0 or ... or ( len g) = 2;

      per cases ;

        suppose f is empty;

        hence thesis by A6, A5, FINSEQ_1: 34;

      end;

        suppose ( len g) = 0 ;

        then g = {} ;

        then c = ( <*> the carrier of ( TOP-REAL 2)) by A5, FINSEQ_6: 80;

        hence thesis by A1, A6, FINSEQ_1: 34;

      end;

        suppose ( len g) = 1;

        then c = {} by A5, FINSEQ_6: 167;

        hence thesis by A1, A6, FINSEQ_1: 34;

      end;

        suppose that

         A7: f is non empty and

         A8: ( len g) = (1 + 1);

        

         A9: (k + 1) = ( len f) by A7, NAT_1: 14, XREAL_1: 235;

        (g | ( len g)) = g by FINSEQ_1: 58;

        then g = <*(g /. 1), (g /. 2)*> by A8, FINSEQ_5: 81;

        then

         A10: (f ^' g) = (f ^ <*(g /. 2)*>) by A6, A5, FINSEQ_6: 46;

        1 <= (( len g) - 1) by A8;

        then 1 <= ( len (g /^ 1)) by A8, RFINSEQ:def 1;

        then

         A11: 1 in ( dom (g /^ 1)) by FINSEQ_3: 25;

        

        then

         A12: (c /. 1) = ((g /^ 1) . 1) by A5, PARTFUN1:def 6

        .= (g . (1 + 1)) by A8, A11, RFINSEQ:def 1

        .= (g /. (1 + 1)) by A8, FINSEQ_4: 15;

        then ( LSeg (g,1)) = ( LSeg ((f /. ( len f)),(c /. 1))) by A3, A8, TOPREAL1:def 3;

        hence thesis by A1, A4, A9, A10, A12, SPPOL_2: 30;

      end;

        suppose that

         A13: f is non empty and

         A14: 2 < ( len g);

        

         A15: 1 <= ( len g) by A14, XXREAL_0: 2;

        then

         A16: ( LSeg ((g /^ 1),1)) = ( LSeg (g,(1 + 1))) by SPPOL_2: 4;

        (1 + 1) <= ( len g) by A14;

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

        then 1 <= ( len (g /^ 1)) by A15, RFINSEQ:def 1;

        then

         A17: 1 in ( dom (g /^ 1)) by FINSEQ_3: 25;

        

        then

         A18: (c /. 1) = ((g /^ 1) . 1) by A5, PARTFUN1:def 6

        .= (g . (1 + 1)) by A15, A17, RFINSEQ:def 1

        .= (g /. (1 + 1)) by A14, FINSEQ_4: 15;

        then

         A19: ( LSeg (g,1)) = ( LSeg ((f /. ( len f)),(c /. 1))) by A3, A14, TOPREAL1:def 3;

        

         A20: (k + 1) = ( len f) by A13, NAT_1: 14, XREAL_1: 235;

        (1 + 2) <= ( len g) by A14, NAT_1: 13;

        then (( LSeg (g,1)) /\ ( LSeg (c,1))) = {(c /. 1)} by A5, A18, A16, TOPREAL1:def 6;

        hence thesis by A1, A4, A6, A5, A20, A19, SPPOL_2: 31;

      end;

    end;

    theorem :: TOPREAL8:35

    

     Th35: f is non empty & g is non trivial & (f /. ( len f)) = (g /. 1) implies ( L~ (f ^' g)) = (( L~ f) \/ ( L~ g))

    proof

      assume that

       A1: f is non empty and

       A2: g is non trivial and

       A3: (f /. ( len f)) = (g /. 1);

      set c = (((1 + 1),( len g)) -cut g);

      

       A4: c = (g /^ 1) by Th13;

      

       A5: ( len g) > 1 by A2, Th2;

      then ( len c) = (( len g) - 1) by A4, RFINSEQ:def 1;

      then ( len c) > (1 - 1) by A5, XREAL_1: 9;

      then ( len c) > 0 ;

      then

       A6: c is non empty;

       not g is empty by A2;

      then g = ( <*(g /. 1)*> ^ c) by A4, FINSEQ_5: 29;

      then

       A7: (( LSeg ((g /. 1),(c /. 1))) \/ ( L~ c)) = ( L~ g) by A6, SPPOL_2: 20;

      ( L~ (f ^ c)) = ((( L~ f) \/ ( LSeg ((f /. ( len f)),(c /. 1)))) \/ ( L~ c)) by A1, A6, SPPOL_2: 23

      .= (( L~ f) \/ (( LSeg ((g /. 1),(c /. 1))) \/ ( L~ c))) by A3, XBOOLE_1: 4;

      hence thesis by A7, FINSEQ_6:def 5;

    end;

    theorem :: TOPREAL8:36

    (for n be Nat st n in ( dom f) holds ex i,j be Nat st [i, j] in ( Indices G) & (f /. n) = (G * (i,j))) & f is non constant circular unfolded s.c.c. special & ( len f) > 4 implies ex g st g is_sequence_on G & g is unfolded s.c.c. special & ( L~ f) = ( L~ g) & (f /. 1) = (g /. 1) & (f /. ( len f)) = (g /. ( len g)) & ( len f) <= ( len g)

    proof

      assume that

       A1: for n be Nat st n in ( dom f) holds ex i,j be Nat st [i, j] in ( Indices G) & (f /. n) = (G * (i,j)) and

       A2: f is non constant circular unfolded and

       A3: f is s.c.c. and

       A4: f is special and

       A5: ( len f) > 4;

      reconsider f9 = f as non constant unfolded s.c.c. special circular FinSequence of ( TOP-REAL 2) by A2, A3, A4;

      reconsider f9 as non constant unfolded s.c.c. special circular non empty FinSequence of ( TOP-REAL 2);

      set h1 = (f9 | 2), h2 = (f9 /^ 1);

      

       A6: ( len f) > (1 + 1) by A2, Th3;

      then

       A7: ( len h1) = (1 + 1) by FINSEQ_1: 59;

      then

      reconsider h1 as non trivial FinSequence of ( TOP-REAL 2) by NAT_D: 60;

      

       A8: h1 is s.n.c. by A6, Th20;

      ( len h1) in ( dom h1) by A7, FINSEQ_3: 25;

      then

       A9: (h1 /. ( len h1)) = (f /. (1 + 1)) by A7, FINSEQ_4: 70;

      1 <= ( len f) by A2, Th3, XXREAL_0: 2;

      then

       A10: ( len h2) = (( len f) - 1) by RFINSEQ:def 1;

      then

       A11: (( len h2) + 1) = ( len f);

      

       A12: ( dom h1) c= ( dom f) by FINSEQ_5: 18;

      

       A13: for n be Nat st n in ( dom h1) holds ex i,j be Nat st [i, j] in ( Indices G) & (h1 /. n) = (G * (i,j))

      proof

        let n be Nat;

        assume

         A14: n in ( dom h1);

        then

        consider i,j be Nat such that

         A15: [i, j] in ( Indices G) and

         A16: (f /. n) = (G * (i,j)) by A1, A12;

        reconsider i, j as Nat;

        take i, j;

        thus [i, j] in ( Indices G) by A15;

        thus thesis by A14, A16, FINSEQ_4: 70;

      end;

      h1 is one-to-one by A5, Th3, Th22;

      then

      consider g1 such that

       A17: g1 is_sequence_on G and

       A18: g1 is one-to-one unfolded s.n.c. special and

       A19: ( L~ h1) = ( L~ g1) and

       A20: (h1 /. 1) = (g1 /. 1) and

       A21: (h1 /. ( len h1)) = (g1 /. ( len g1)) and

       A22: ( len h1) <= ( len g1) by A13, A8, GOBOARD3: 1;

      reconsider g1 as non trivial FinSequence of ( TOP-REAL 2) by A7, A22, NAT_D: 60;

      

       A23: 1 <= (( len g1) -' 1) by A7, A22, NAT_D: 55;

      ((( len g1) -' 1) + 1) = ( len g1) by A7, A22, XREAL_1: 235, XXREAL_0: 2;

      then

       A24: (g1 /. ( len g1)) in ( LSeg (g1,(( len g1) -' 1))) by A23, TOPREAL1: 21;

      

       A25: ( LSeg (g1,(( len g1) -' 1))) c= ( L~ g1) by TOPREAL3: 19;

      

       A26: ( len h2) > ((1 + 1) - 1) by A6, A10, XREAL_1: 9;

      then

       A27: ( len h2) >= 2 by NAT_1: 13;

      then

      reconsider h2 as non trivial FinSequence of ( TOP-REAL 2) by NAT_D: 60;

      

       A28: h2 is s.n.c. by Th21;

      

       A29: ( len h2) in ( dom h2) by FINSEQ_5: 6;

      

       A30: 1 in ( dom h1) by FINSEQ_5: 6;

      then

       A31: (h1 /. 1) = (f /. 1) by FINSEQ_4: 70;

      

      then

       A32: (h1 /. 1) = (f /. ( len f)) by FINSEQ_6:def 1

      .= (h2 /. ( len h2)) by A11, A29, FINSEQ_5: 27;

      

       A33: for n be Nat st n in ( dom h2) holds ex i,j be Nat st [i, j] in ( Indices G) & (h2 /. n) = (G * (i,j))

      proof

        let n be Nat;

        assume

         A34: n in ( dom h2);

        then

        consider i,j be Nat such that

         A35: [i, j] in ( Indices G) and

         A36: (f /. (n + 1)) = (G * (i,j)) by A1, FINSEQ_5: 26;

        reconsider i, j as Nat;

        take i, j;

        thus [i, j] in ( Indices G) by A35;

        thus thesis by A34, A36, FINSEQ_5: 27;

      end;

      h2 is one-to-one by A5, Th24;

      then

      consider g2 such that

       A37: g2 is_sequence_on G and

       A38: g2 is one-to-one unfolded s.n.c. special and

       A39: ( L~ h2) = ( L~ g2) and

       A40: (h2 /. 1) = (g2 /. 1) and

       A41: (h2 /. ( len h2)) = (g2 /. ( len g2)) and

       A42: ( len h2) <= ( len g2) by A33, A28, GOBOARD3: 1;

      

       A43: ( len g2) >= (1 + 1) by A27, A42, XXREAL_0: 2;

      then

      reconsider g2 as non trivial FinSequence of ( TOP-REAL 2) by NAT_D: 60;

      

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

      

       A45: ( LSeg (g2,1)) c= ( L~ g2) by TOPREAL3: 19;

      take g = (g1 ^' g2);

      1 in ( dom h2) by A26, FINSEQ_3: 25;

      then

       A46: (h1 /. ( len h1)) = (h2 /. 1) by A9, FINSEQ_5: 27;

      hence g is_sequence_on G by A17, A21, A37, A40, Th12;

      (( LSeg (f,1)) /\ ( L~ h2)) = {(h1 /. 1), (h2 /. 1)} by A5, A9, A46, A31, Th27;

      then

       A47: (( L~ g1) /\ ( L~ g2)) = {(g1 /. 1), (g2 /. 1)} by A19, A20, A39, A40, Th19;

      ( len h2) > ((3 + 1) - 1) by A5, A10, XREAL_1: 9;

      then (2 + 1) < ( len g2) by A42, XXREAL_0: 2;

      then

       A48: (1 + 1) < (( len g2) -' 1) by NAT_D: 52;

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

      then

       A49: (g2 /. ( len g2)) in ( LSeg (g2,(( len g2) -' 1))) by A44, TOPREAL1: 21;

      ( LSeg (g2,1)) misses ( LSeg (g2,(( len g2) -' 1))) by A38, A48;

      then not (g2 /. ( len g2)) in ( LSeg (g2,1)) by A49, XBOOLE_0: 3;

      then

       A50: not (g2 /. ( len g2)) in (( LSeg (g1,(( len g1) -' 1))) /\ ( LSeg (g2,1))) by XBOOLE_0:def 4;

      (g2 /. 1) in ( LSeg (g2,1)) by A43, TOPREAL1: 21;

      then (g2 /. 1) in (( LSeg (g1,(( len g1) -' 1))) /\ ( LSeg (g2,1))) by A21, A40, A46, A24, XBOOLE_0:def 4;

      then (( LSeg (g1,(( len g1) -' 1))) /\ ( LSeg (g2,1))) = {(g2 /. 1)} by A20, A41, A32, A47, A50, A25, A45, Th1, XBOOLE_1: 27;

      hence g is unfolded by A18, A21, A38, A40, A46, Th34;

      thus g is s.c.c. by A18, A20, A21, A38, A40, A41, A46, A32, A47, Th33;

      thus g is special by A18, A21, A38, A40, A46, Th26;

      

       A51: (((1 + 1),( len h2)) -cut h2) = (h2 /^ 1) by Th13;

      

       A52: f = (h1 ^ (f /^ (1 + 1))) by RFINSEQ: 8

      .= (h1 ^ ((2,( len h2)) -cut h2)) by A51, FINSEQ_6: 81

      .= (h1 ^' h2) by FINSEQ_6:def 5;

      then

       A53: (( len f) + 1) = (( len h1) + ( len h2)) by FINSEQ_6: 139;

      

      thus ( L~ f) = (( L~ h1) \/ ( L~ h2)) by A52, A46, Th35

      .= ( L~ g) by A19, A21, A39, A40, A46, Th35;

      

      thus (f /. 1) = (h1 /. 1) by A30, FINSEQ_4: 70

      .= (g /. 1) by A20, FINSEQ_6: 155;

      

      thus (f /. ( len f)) = (h2 /. ( len h2)) by A11, A29, FINSEQ_5: 27

      .= (g /. ( len g)) by A41, FINSEQ_6: 156;

      (( len g) + 1) = (( len g1) + ( len g2)) by FINSEQ_6: 139;

      then (( len f) + 1) <= (( len g) + 1) by A22, A42, A53, XREAL_1: 7;

      hence thesis by XREAL_1: 6;

    end;