sppol_2.miz



    begin

    reserve P for Subset of ( TOP-REAL 2),

f,f1,f2,g for FinSequence of ( TOP-REAL 2),

p,p1,p2,q,q1,q2 for Point of ( TOP-REAL 2),

r1,r2,r19,r29 for Real,

i,j,k,n for Nat;

    theorem :: SPPOL_2:1

     |[r1, r2]| = |[r19, r29]| implies r1 = r19 & r2 = r29 by FINSEQ_1: 77;

    theorem :: SPPOL_2:2

    

     Th2: for i,j be Nat holds (i + j) = ( len f) implies ( LSeg (f,i)) = ( LSeg (( Rev f),j))

    proof

      let i,j be Nat;

      assume

       A1: (i + j) = ( len f);

      per cases ;

        suppose that

         A2: 1 <= i and

         A3: (i + 1) <= ( len f);

        

         A4: (i + (j + 1)) = (( len f) + 1) by A1;

        

         A5: i in ( dom f) by A2, A3, SEQ_4: 134;

        then (j + 1) in ( dom ( Rev f)) by A4, FINSEQ_5: 59;

        then

         A6: (j + 1) <= ( len ( Rev f)) by FINSEQ_3: 25;

        

         A7: ((i + 1) + j) = (( len f) + 1) by A1;

        

         A8: (i + 1) in ( dom f) by A2, A3, SEQ_4: 134;

        then j in ( dom ( Rev f)) by A7, FINSEQ_5: 59;

        then

         A9: 1 <= j by FINSEQ_3: 25;

        

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

        .= ( LSeg ((( Rev f) /. (j + 1)),(f /. (i + 1)))) by A5, A4, FINSEQ_5: 66

        .= ( LSeg ((( Rev f) /. j),(( Rev f) /. (j + 1)))) by A8, A7, FINSEQ_5: 66

        .= ( LSeg (( Rev f),j)) by A6, A9, TOPREAL1:def 3;

      end;

        suppose

         A10: not 1 <= i;

        then i = 0 by NAT_1: 14;

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

        then

         A11: not (j + 1) <= ( len ( Rev f)) by FINSEQ_5:def 3;

        ( LSeg (f,i)) = {} by A10, TOPREAL1:def 3;

        hence thesis by A11, TOPREAL1:def 3;

      end;

        suppose

         A12: not (i + 1) <= ( len f);

        then

         A13: ( LSeg (f,i)) = {} by TOPREAL1:def 3;

        j < 1 by A1, A12, XREAL_1: 6;

        hence thesis by A13, TOPREAL1:def 3;

      end;

    end;

    theorem :: SPPOL_2:3

    

     Th3: for i,n be Nat holds (i + 1) <= ( len (f | n)) implies ( LSeg ((f | n),i)) = ( LSeg (f,i))

    proof

      let i,n be Nat;

      assume

       A1: (i + 1) <= ( len (f | n));

      per cases ;

        suppose i <> 0 ;

        then

         A2: 1 <= i by NAT_1: 14;

        then

         A3: i in ( dom (f | n)) by A1, SEQ_4: 134;

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

        then

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

        

         A5: (i + 1) in ( dom (f | n)) by A1, A2, SEQ_4: 134;

        

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

        .= ( LSeg ((f /. i),((f | n) /. (i + 1)))) by A3, FINSEQ_4: 70

        .= ( LSeg ((f /. i),(f /. (i + 1)))) by A5, FINSEQ_4: 70

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

      end;

        suppose

         A6: i = 0 ;

        

        hence ( LSeg ((f | n),i)) = {} by TOPREAL1:def 3

        .= ( LSeg (f,i)) by A6, TOPREAL1:def 3;

      end;

    end;

    theorem :: SPPOL_2:4

    

     Th4: for i,n be Nat holds n <= ( len f) & 1 <= i implies ( LSeg ((f /^ n),i)) = ( LSeg (f,(n + i)))

    proof

      let i,n be Nat;

      assume that

       A1: n <= ( len f) and

       A2: 1 <= i;

      per cases ;

        suppose

         A3: (i + 1) <= (( len f) - n);

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

        then 1 <= (( len f) - n) by A3, XXREAL_0: 2;

        then

         A4: (1 + n) <= ( len f) by XREAL_1: 19;

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

        then n <= ( len f) by A4, XXREAL_0: 2;

        then

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

        then

         A6: i in ( dom (f /^ n)) by A2, A3, SEQ_4: 134;

        

         A7: ((i + 1) + n) <= ( len f) by A3, XREAL_1: 19;

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

        then

         A8: 1 <= (i + n) by A2, XXREAL_0: 2;

        

         A9: (i + 1) in ( dom (f /^ n)) by A2, A3, A5, SEQ_4: 134;

        

        thus ( LSeg ((f /^ n),i)) = ( LSeg (((f /^ n) /. i),((f /^ n) /. (i + 1)))) by A2, A3, A5, TOPREAL1:def 3

        .= ( LSeg ((f /. (i + n)),((f /^ n) /. (i + 1)))) by A6, FINSEQ_5: 27

        .= ( LSeg ((f /. (i + n)),(f /. ((i + 1) + n)))) by A9, FINSEQ_5: 27

        .= ( LSeg ((f /. (i + n)),(f /. ((i + n) + 1))))

        .= ( LSeg (f,(n + i))) by A8, A7, TOPREAL1:def 3;

      end;

        suppose

         A10: (i + 1) > (( len f) - n);

        then (n + (i + 1)) > ( len f) by XREAL_1: 19;

        then

         A11: ((n + i) + 1) > ( len f);

        (i + 1) > ( len (f /^ n)) by A1, A10, RFINSEQ:def 1;

        

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

        .= ( LSeg (f,(n + i))) by A11, TOPREAL1:def 3;

      end;

    end;

    theorem :: SPPOL_2:5

    

     Th5: for i,n be Nat holds 1 <= i & (i + 1) <= (( len f) - n) implies ( LSeg ((f /^ n),i)) = ( LSeg (f,(n + i)))

    proof

      let i,n be Nat;

      assume

       A1: 1 <= i;

      

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

      assume (i + 1) <= (( len f) - n);

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

      then n <= ( len f) by A2, XXREAL_0: 2;

      hence thesis by A1, Th4;

    end;

    theorem :: SPPOL_2:6

    

     Th6: for i be Nat holds (i + 1) <= ( len f) implies ( LSeg ((f ^ g),i)) = ( LSeg (f,i))

    proof

      let i be Nat;

      assume

       A1: (i + 1) <= ( len f);

      per cases ;

        suppose i <> 0 ;

        then

         A2: 1 <= i by NAT_1: 14;

        then

         A3: i in ( dom f) by A1, SEQ_4: 134;

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

        then ( len (f ^ g)) >= ( len f) by NAT_1: 11;

        then

         A4: (i + 1) <= ( len (f ^ g)) by A1, XXREAL_0: 2;

        

         A5: (i + 1) in ( dom f) by A1, A2, SEQ_4: 134;

        

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

        .= ( LSeg (((f ^ g) /. i),(f /. (i + 1)))) by A3, FINSEQ_4: 68

        .= ( LSeg (((f ^ g) /. i),((f ^ g) /. (i + 1)))) by A5, FINSEQ_4: 68

        .= ( LSeg ((f ^ g),i)) by A2, A4, TOPREAL1:def 3;

      end;

        suppose

         A6: i = 0 ;

        

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

        .= ( LSeg (f,i)) by A6, TOPREAL1:def 3;

      end;

    end;

    theorem :: SPPOL_2:7

    

     Th7: for i be Nat holds 1 <= i implies ( LSeg ((f ^ g),(( len f) + i))) = ( LSeg (g,i))

    proof

      let i be Nat;

      assume

       A1: 1 <= i;

      per cases ;

        suppose

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

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

        then ((( len f) + i) + 1) <= (( len f) + ( len g)) by A2, XREAL_1: 6;

        then

         A3: ((( len f) + i) + 1) <= ( len (f ^ g)) by FINSEQ_1: 22;

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

        then

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

        

         A5: (i + 1) in ( dom g) by A1, A2, SEQ_4: 134;

        

         A6: i in ( dom g) by A1, A2, SEQ_4: 134;

        

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

        .= ( LSeg (((f ^ g) /. (( len f) + i)),(g /. (i + 1)))) by A6, FINSEQ_4: 69

        .= ( LSeg (((f ^ g) /. (( len f) + i)),((f ^ g) /. (( len f) + (i + 1))))) by A5, FINSEQ_4: 69

        .= ( LSeg ((f ^ g),(( len f) + i))) by A4, A3, TOPREAL1:def 3;

      end;

        suppose

         A7: (i + 1) > ( len g);

        then (( len f) + (i + 1)) > (( len f) + ( len g)) by XREAL_1: 6;

        then ((( len f) + i) + 1) > ( len (f ^ g)) by FINSEQ_1: 22;

        

        hence ( LSeg ((f ^ g),(( len f) + i))) = {} by TOPREAL1:def 3

        .= ( LSeg (g,i)) by A7, TOPREAL1:def 3;

      end;

    end;

    theorem :: SPPOL_2:8

    

     Th8: f is non empty & g is non empty implies ( LSeg ((f ^ g),( len f))) = ( LSeg ((f /. ( len f)),(g /. 1)))

    proof

      assume that

       A1: f is non empty and

       A2: g is non empty;

      

       A3: 1 in ( dom g) by A2, FINSEQ_5: 6;

      then 1 <= ( len g) by FINSEQ_3: 25;

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

      then

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

      

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

      then 1 <= ( len f) by FINSEQ_3: 25;

      

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

      .= ( LSeg ((f /. ( len f)),((f ^ g) /. (( len f) + 1)))) by A5, FINSEQ_4: 68

      .= ( LSeg ((f /. ( len f)),(g /. 1))) by A3, FINSEQ_4: 69;

    end;

    theorem :: SPPOL_2:9

    

     Th9: for i be Nat holds (i + 1) <= ( len (f -: p)) implies ( LSeg ((f -: p),i)) = ( LSeg (f,i))

    proof

      let i be Nat;

      (f -: p) = (f | (p .. f)) by FINSEQ_5:def 1;

      hence thesis by Th3;

    end;

    theorem :: SPPOL_2:10

    

     Th10: for i be Nat holds p in ( rng f) implies ( LSeg ((f :- p),(i + 1))) = ( LSeg (f,(i + (p .. f))))

    proof

      let i be Nat;

      

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

      assume

       A2: p in ( rng f);

      then

       A3: ( len (f :- p)) = ((( len f) - (p .. f)) + 1) by FINSEQ_5: 50;

      

       A4: (i + (1 + 1)) = ((i + 1) + 1);

      per cases ;

        suppose

         A5: (i + 2) <= ( len (f :- p));

        then (i + 1) <= (( len f) - (p .. f)) by A4, A3, XREAL_1: 6;

        then

         A6: ((i + 1) + (p .. f)) <= ( len f) by XREAL_1: 19;

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

        then (i + 1) <= (i + (p .. f)) by XREAL_1: 6;

        then

         A7: 1 <= (i + (p .. f)) by A1, XXREAL_0: 2;

        

         A8: (i + 1) in ( dom (f :- p)) by A1, A4, A5, SEQ_4: 134;

        

         A9: ((i + 1) + 1) in ( dom (f :- p)) by A1, A5, SEQ_4: 134;

        

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

        .= ( LSeg ((f /. (i + (p .. f))),((f :- p) /. ((i + 1) + 1)))) by A2, A8, FINSEQ_5: 52

        .= ( LSeg ((f /. (i + (p .. f))),(f /. ((i + 1) + (p .. f))))) by A2, A9, FINSEQ_5: 52

        .= ( LSeg ((f /. (i + (p .. f))),(f /. ((i + (p .. f)) + 1))))

        .= ( LSeg (f,(i + (p .. f)))) by A7, A6, TOPREAL1:def 3;

      end;

        suppose

         A10: (i + 2) > ( len (f :- p));

        then (i + 1) > (( len f) - (p .. f)) by A4, A3, XREAL_1: 6;

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

        then ((i + (p .. f)) + 1) > ( len f);

        

        hence ( LSeg (f,(i + (p .. f)))) = {} by TOPREAL1:def 3

        .= ( LSeg ((f :- p),(i + 1))) by A4, A10, TOPREAL1:def 3;

      end;

    end;

    theorem :: SPPOL_2:11

    

     Th11: ( L~ ( <*> the carrier of ( TOP-REAL 2))) = {} by TOPREAL1: 22;

    theorem :: SPPOL_2:12

    

     Th12: ( L~ <*p*>) = {} by FINSEQ_1: 39, TOPREAL1: 22;

    theorem :: SPPOL_2:13

    

     Th13: p in ( L~ f) implies ex i st 1 <= i & (i + 1) <= ( len f) & p in ( LSeg (f,i))

    proof

      set X = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) };

      assume p in ( L~ f);

      then

      consider Y be set such that

       A1: p in Y and

       A2: Y in X by TARSKI:def 4;

      ex i st Y = ( LSeg (f,i)) & 1 <= i & (i + 1) <= ( len f) by A2;

      hence thesis by A1;

    end;

    theorem :: SPPOL_2:14

    

     Th14: p in ( L~ f) implies ex i st 1 <= i & (i + 1) <= ( len f) & p in ( LSeg ((f /. i),(f /. (i + 1))))

    proof

      assume p in ( L~ f);

      then

      consider i such that

       A1: 1 <= i and

       A2: (i + 1) <= ( len f) and

       A3: p in ( LSeg (f,i)) by Th13;

      take i;

      thus 1 <= i & (i + 1) <= ( len f) by A1, A2;

      thus thesis by A1, A2, A3, TOPREAL1:def 3;

    end;

    theorem :: SPPOL_2:15

    

     Th15: 1 <= i & (i + 1) <= ( len f) & p in ( LSeg ((f /. i),(f /. (i + 1)))) implies p in ( L~ f)

    proof

      assume that

       A1: 1 <= i and

       A2: (i + 1) <= ( len f) and

       A3: p in ( LSeg ((f /. i),(f /. (i + 1))));

      set X = { ( LSeg (f,j)) : 1 <= j & (j + 1) <= ( len f) };

      

       A4: ( LSeg (f,i)) in X by A1, A2;

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

      hence thesis by A3, A4, TARSKI:def 4;

    end;

    theorem :: SPPOL_2:16

    1 <= i & (i + 1) <= ( len f) implies ( LSeg ((f /. i),(f /. (i + 1)))) c= ( L~ f)

    proof

      assume that

       A1: 1 <= i and

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

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

      hence thesis by TOPREAL3: 19;

    end;

    theorem :: SPPOL_2:17

    p in ( LSeg (f,i)) implies p in ( L~ f)

    proof

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

      hence thesis;

    end;

    theorem :: SPPOL_2:18

    

     Th18: ( len f) >= 2 implies ( rng f) c= ( L~ f)

    proof

      assume

       A1: ( len f) >= 2;

      let x be object;

      assume x in ( rng f);

      then

      consider i be Element of NAT such that

       A2: i in ( dom f) and

       A3: (f /. i) = x by PARTFUN2: 2;

      

       A4: 1 <= i by A2, FINSEQ_3: 25;

      

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

      

       A6: (f /. i) in ( LSeg ((f /. i),(f /. (i + 1)))) by RLTOPSP1: 68;

      per cases ;

        suppose

         A7: i = ( len f);

        then

        consider j be Nat such that

         A8: (j + 1) = i by A1, NAT_1: 6;

        reconsider j as Element of NAT by ORDINAL1:def 12;

        (1 + 1) <= (j + 1) by A1, A7, A8;

        then

         A9: 1 <= j by XREAL_1: 6;

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

        hence thesis by A3, A7, A8, A9, Th15;

      end;

        suppose i <> ( len f);

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

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

        hence thesis by A3, A4, A6, Th15;

      end;

    end;

    theorem :: SPPOL_2:19

    

     Th19: f is non empty implies ( L~ (f ^ <*p*>)) = (( L~ f) \/ ( LSeg ((f /. ( len f)),p)))

    proof

      set fp = (f ^ <*p*>);

      

       A1: (( len f) + 1) <= ( len fp) by FINSEQ_2: 16;

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

      then

       A2: (( len f) + 1) in ( dom fp) by A1, FINSEQ_3: 25;

      

       A3: (fp /. (( len f) + 1)) = p by FINSEQ_4: 67;

      ( len fp) = (( len f) + 1) by FINSEQ_2: 16;

      then

       A4: (fp | (( len f) + 1)) = fp by FINSEQ_1: 58;

      

       A5: ( dom f) c= ( dom fp) by FINSEQ_1: 26;

      

       A6: (fp | ( len f)) = f by FINSEQ_5: 23;

      assume f is non empty;

      then

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

      then (fp /. ( len f)) = (f /. ( len f)) by FINSEQ_4: 68;

      hence thesis by A2, A7, A3, A4, A5, A6, TOPREAL3: 38;

    end;

    theorem :: SPPOL_2:20

    

     Th20: f is non empty implies ( L~ ( <*p*> ^ f)) = (( LSeg (p,(f /. 1))) \/ ( L~ f))

    proof

      set q = (f /. 1);

      

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

      then

       A2: ( len ( <*p*> ^ f)) = (1 + ( len f)) by FINSEQ_1: 22;

      assume that

       A3: f is non empty;

      hereby

        let x be object;

        assume

         A4: x in ( L~ ( <*p*> ^ f));

        then

        reconsider r = x as Point of ( TOP-REAL 2);

        consider i such that

         A5: 1 <= i and

         A6: (i + 1) <= ( len ( <*p*> ^ f)) and

         A7: r in ( LSeg ((( <*p*> ^ f) /. i),(( <*p*> ^ f) /. (i + 1)))) by A4, Th14;

        now

          per cases by A5, XXREAL_0: 1;

            case

             A8: i = 1;

            then

             A9: p = (( <*p*> ^ f) /. i) by FINSEQ_5: 15;

            i in ( dom f) by A3, A8, FINSEQ_5: 6;

            hence r in ( LSeg (p,q)) by A1, A7, A8, A9, FINSEQ_4: 69;

          end;

            case

             A10: i > 1;

            then

            consider j be Nat such that

             A11: i = (j + 1) by NAT_1: 6;

            reconsider j as Element of NAT by ORDINAL1:def 12;

            

             A12: 1 <= j by A10, A11, NAT_1: 13;

            

             A13: (j + 1) <= ( len f) by A2, A6, A11, XREAL_1: 6;

            then (j + 1) in ( dom f) by A12, SEQ_4: 134;

            then

             A14: (( <*p*> ^ f) /. (i + 1)) = (f /. (j + 1)) by A1, A11, FINSEQ_4: 69;

            j in ( dom f) by A12, A13, SEQ_4: 134;

            then (( <*p*> ^ f) /. i) = (f /. j) by A1, A11, FINSEQ_4: 69;

            hence r in ( L~ f) by A7, A12, A13, A14, Th15;

          end;

        end;

        hence x in (( LSeg (p,q)) \/ ( L~ f)) by XBOOLE_0:def 3;

      end;

      let x be object;

      assume

       A15: x in (( LSeg (p,q)) \/ ( L~ f));

      then

      reconsider r = x as Point of ( TOP-REAL 2);

      per cases by A15, XBOOLE_0:def 3;

        suppose

         A16: r in ( LSeg (p,q));

        set i = 1;

        i <= ( len f) by A3, NAT_1: 14;

        then

         A17: (i + 1) <= ( len ( <*p*> ^ f)) by A2, XREAL_1: 6;

        i in ( dom f) by A3, FINSEQ_5: 6;

        then

         A18: q = (( <*p*> ^ f) /. (i + 1)) by A1, FINSEQ_4: 69;

        p = (( <*p*> ^ f) /. i) by FINSEQ_5: 15;

        hence thesis by A16, A17, A18, Th15;

      end;

        suppose r in ( L~ f);

        then

        consider j such that

         A19: 1 <= j and

         A20: (j + 1) <= ( len f) and

         A21: r in ( LSeg ((f /. j),(f /. (j + 1)))) by Th14;

        set i = (j + 1);

        j in ( dom f) by A19, A20, SEQ_4: 134;

        then

         A22: (( <*p*> ^ f) /. i) = (f /. j) by A1, FINSEQ_4: 69;

        (j + 1) in ( dom f) by A19, A20, SEQ_4: 134;

        then

         A23: (( <*p*> ^ f) /. (i + 1)) = (f /. (j + 1)) by A1, FINSEQ_4: 69;

        (i + 1) <= ( len ( <*p*> ^ f)) by A2, A20, XREAL_1: 6;

        hence thesis by A21, A22, A23, Th15, NAT_1: 12;

      end;

    end;

    theorem :: SPPOL_2:21

    

     Th21: ( L~ <*p, q*>) = ( LSeg (p,q))

    proof

      set f = <*p*>;

      

       A1: ( len f) = 1 by FINSEQ_1: 39;

      

      thus ( L~ <*p, q*>) = ( L~ (f ^ <*q*>)) by FINSEQ_1:def 9

      .= (( L~ f) \/ ( LSeg ((f /. ( len f)),q))) by Th19

      .= (( L~ f) \/ ( LSeg (p,q))) by A1, FINSEQ_4: 16

      .= ( {} \/ ( LSeg (p,q))) by A1, TOPREAL1: 22

      .= ( LSeg (p,q));

    end;

    theorem :: SPPOL_2:22

    

     Th22: ( L~ f) = ( L~ ( Rev f))

    proof

      defpred P[ FinSequence of ( TOP-REAL 2)] means ( L~ $1) = ( L~ ( Rev $1));

      

       A1: for f, p st P[f] holds P[(f ^ <*p*>)]

      proof

        let f, p such that

         A2: P[f];

        per cases ;

          suppose

           A3: f is empty;

          

          hence ( L~ (f ^ <*p*>)) = ( L~ <*p*>) by FINSEQ_1: 34

          .= ( L~ ( Rev <*p*>)) by FINSEQ_5: 60

          .= ( L~ ( Rev (f ^ <*p*>))) by A3, FINSEQ_1: 34;

        end;

          suppose

           A4: f is non empty;

          set q9 = (( Rev f) /. 1);

          set q = (f /. ( len f));

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

          then

           A5: ( Rev f) is non empty by A4;

          q = q9 by A4, FINSEQ_5: 65;

          

          hence ( L~ (f ^ <*p*>)) = (( LSeg (p,q9)) \/ ( L~ ( Rev f))) by A2, A4, Th19

          .= ( L~ ( <*p*> ^ ( Rev f))) by A5, Th20

          .= ( L~ ( Rev (f ^ <*p*>))) by FINSEQ_5: 63;

        end;

      end;

      

       A6: P[( <*> the carrier of ( TOP-REAL 2))];

      for f holds P[f] from FINSEQ_2:sch 2( A6, A1);

      hence thesis;

    end;

    theorem :: SPPOL_2:23

    

     Th23: f1 is non empty & f2 is non empty implies ( L~ (f1 ^ f2)) = ((( L~ f1) \/ ( LSeg ((f1 /. ( len f1)),(f2 /. 1)))) \/ ( L~ f2))

    proof

      set p = (f1 /. ( len f1)), q = (f2 /. 1);

      defpred P[ FinSequence of ( TOP-REAL 2)] means ( L~ ((f1 ^ <*q*>) ^ $1)) = ((( L~ f1) \/ ( LSeg (p,q))) \/ ( L~ ( <*q*> ^ $1)));

      assume

       A1: f1 is non empty;

      

       A2: for f holds for o be Point of ( TOP-REAL 2) st P[f] holds P[(f ^ <*o*>)]

      proof

        let f;

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

         A3: P[f];

        per cases ;

          suppose f is empty;

          then

           A4: (f ^ <*o*>) = <*o*> by FINSEQ_1: 34;

          ( len (f1 ^ <*q*>)) = (( len f1) + 1) by FINSEQ_2: 16;

          then ((f1 ^ <*q*>) /. ( len (f1 ^ <*q*>))) = q by FINSEQ_4: 67;

          

          hence ( L~ ((f1 ^ <*q*>) ^ (f ^ <*o*>))) = (( L~ (f1 ^ <*q*>)) \/ ( LSeg (q,o))) by A4, Th19

          .= ((( L~ f1) \/ ( LSeg (p,q))) \/ ( LSeg (q,o))) by A1, Th19

          .= ((( L~ f1) \/ ( LSeg (p,q))) \/ ( L~ <*q, o*>)) by Th21

          .= ((( L~ f1) \/ ( LSeg (p,q))) \/ ( L~ ( <*q*> ^ (f ^ <*o*>)))) by A4, FINSEQ_1:def 9;

        end;

          suppose

           A5: f is non empty;

          set g = ((f1 ^ <*q*>) ^ f), h = ( <*q*> ^ f);

          ( len f) <> 0 by A5;

          then

          consider f9 be FinSequence of ( TOP-REAL 2), d be Point of ( TOP-REAL 2) such that

           A6: f = (f9 ^ <*d*>) by FINSEQ_2: 19;

          

           A7: h = (( <*q*> ^ f9) ^ <*d*>) by A6, FINSEQ_1: 32;

          then ( len h) = (( len ( <*q*> ^ f9)) + 1) by FINSEQ_2: 16;

          then

           A8: (h /. ( len h)) = d by A7, FINSEQ_4: 67;

          

           A9: g = (((f1 ^ <*q*>) ^ f9) ^ <*d*>) by A6, FINSEQ_1: 32;

          then ( len g) = (( len ((f1 ^ <*q*>) ^ f9)) + 1) by FINSEQ_2: 16;

          then (g /. ( len g)) = d by A9, FINSEQ_4: 67;

          

          then

           A10: (( L~ h) \/ ( LSeg ((g /. ( len g)),o))) = ( L~ (h ^ <*o*>)) by A8, Th19

          .= ( L~ ( <*q*> ^ (f ^ <*o*>))) by FINSEQ_1: 32;

          

          thus ( L~ ((f1 ^ <*q*>) ^ (f ^ <*o*>))) = ( L~ (g ^ <*o*>)) by FINSEQ_1: 32

          .= (( L~ g) \/ ( LSeg ((g /. ( len g)),o))) by Th19

          .= ((( L~ f1) \/ ( LSeg (p,q))) \/ ( L~ ( <*q*> ^ (f ^ <*o*>)))) by A3, A10, XBOOLE_1: 4;

        end;

      end;

      assume f2 is non empty;

      then

       A11: f2 = ( <*q*> ^ (f2 /^ 1)) by FINSEQ_5: 29;

      

       A12: P[( <*> the carrier of ( TOP-REAL 2))]

      proof

        set O = ( <*> the carrier of ( TOP-REAL 2));

        

        thus ( L~ ((f1 ^ <*q*>) ^ O)) = ( L~ (f1 ^ <*q*>)) by FINSEQ_1: 34

        .= ((( L~ f1) \/ ( LSeg (p,q))) \/ {} ) by A1, Th19

        .= ((( L~ f1) \/ ( LSeg (p,q))) \/ ( L~ <*q*>)) by Th12

        .= ((( L~ f1) \/ ( LSeg (p,q))) \/ ( L~ ( <*q*> ^ O))) by FINSEQ_1: 34;

      end;

      for f holds P[f] from FINSEQ_2:sch 2( A12, A2);

      then ( L~ ((f1 ^ <*q*>) ^ (f2 /^ 1))) = ((( L~ f1) \/ ( LSeg (p,q))) \/ ( L~ ( <*q*> ^ (f2 /^ 1))));

      hence thesis by A11, FINSEQ_1: 32;

    end;

    

     Lm1: ( L~ (f | n)) c= ( L~ f)

    proof

      now

        per cases ;

          suppose

           A1: n = 0 ;

          thus thesis by A1, Th11;

        end;

          suppose

           A2: n <> 0 ;

          now

            per cases ;

              suppose

               A3: n < ( len f);

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

              then ( len (f /^ n)) <> 0 by A3;

              then

               A4: (f /^ n) is non empty;

              ( len (f | n)) = n by A3, FINSEQ_1: 59;

              then

               A5: (f | n) is non empty by A2;

              ((f | n) ^ (f /^ n)) = f by RFINSEQ: 8;

              

              then ( L~ f) = ((( L~ (f | n)) \/ ( LSeg (((f | n) /. ( len (f | n))),((f /^ n) /. 1)))) \/ ( L~ (f /^ n))) by A5, A4, Th23

              .= (( L~ (f | n)) \/ (( LSeg (((f | n) /. ( len (f | n))),((f /^ n) /. 1))) \/ ( L~ (f /^ n)))) by XBOOLE_1: 4;

              hence thesis by XBOOLE_1: 7;

            end;

              suppose n >= ( len f);

              hence thesis by FINSEQ_1: 58;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: SPPOL_2:24

    

     Th24: q in ( rng f) implies ( L~ f) = (( L~ (f -: q)) \/ ( L~ (f :- q)))

    proof

      set n = (q .. f);

      assume

       A1: q in ( rng f);

      then

       A2: n <= ( len f) by FINSEQ_4: 21;

      per cases by A2, XXREAL_0: 1;

        suppose

         A3: n < ( len f);

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

        then ( len (f /^ n)) <> 0 by A3;

        then

         A4: (f /^ n) is non empty;

        

         A5: ( len (f | n)) = n by A3, FINSEQ_1: 59;

        (f | n) = (f -: q) by FINSEQ_5:def 1;

        then

         A6: ((f | n) /. ( len (f | n))) = q by A1, A5, FINSEQ_5: 45;

        

         A7: ((f | n) ^ (f /^ n)) = f by RFINSEQ: 8;

        (f | n) is non empty by A1, A5, FINSEQ_4: 21;

        

        hence ( L~ f) = ((( L~ (f | n)) \/ ( LSeg (((f | n) /. ( len (f | n))),((f /^ n) /. 1)))) \/ ( L~ (f /^ n))) by A4, A7, Th23

        .= (( L~ (f | n)) \/ (( LSeg (((f | n) /. ( len (f | n))),((f /^ n) /. 1))) \/ ( L~ (f /^ n)))) by XBOOLE_1: 4

        .= (( L~ (f | n)) \/ ( L~ ( <*((f | n) /. ( len (f | n)))*> ^ (f /^ n)))) by A4, Th20

        .= (( L~ (f | n)) \/ ( L~ (f :- q))) by A6, FINSEQ_5:def 2

        .= (( L~ (f -: q)) \/ ( L~ (f :- q))) by FINSEQ_5:def 1;

      end;

        suppose

         A8: n = ( len f);

        

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

        .= 0 by A8;

        then

         A9: (f /^ n) is empty;

        (f :- q) = ( <*q*> ^ (f /^ n)) by FINSEQ_5:def 2

        .= <*q*> by A9, FINSEQ_1: 34;

        then

         A10: ( L~ (f :- q)) is empty by Th12;

        ( L~ f) = ( L~ (f | n)) by A8, FINSEQ_1: 58

        .= ( L~ (f -: q)) by FINSEQ_5:def 1;

        hence thesis by A10;

      end;

    end;

    theorem :: SPPOL_2:25

    

     Th25: p in ( LSeg (f,n)) implies ( L~ f) = ( L~ ( Ins (f,n,p)))

    proof

      set f1 = (f | n), g1 = (f1 ^ <*p*>), f2 = (f /^ n);

      

       A1: (g1 /. ( len g1)) = (g1 /. (( len f1) + 1)) by FINSEQ_2: 16

      .= p by FINSEQ_4: 67;

      assume

       A2: p in ( LSeg (f,n));

      then

       A3: (n + 1) <= ( len f) by TOPREAL1:def 3;

      then

       A4: 1 <= (( len f) - n) by XREAL_1: 19;

      

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

      then

       A6: ( len f1) = n by A3, FINSEQ_1: 59, XXREAL_0: 2;

      then

       A7: f1 is non empty by A2, TOPREAL1:def 3;

      

       A8: 1 <= n by A2, TOPREAL1:def 3;

      then

       A9: n in ( dom f1) by A6, FINSEQ_3: 25;

      n <= ( len f) by A3, A5, XXREAL_0: 2;

      then 1 <= ( len f2) by A4, RFINSEQ:def 1;

      then

       A10: 1 in ( dom f2) by FINSEQ_3: 25;

      

       A11: ( LSeg (f,n)) = ( LSeg ((f /. n),(f /. (n + 1)))) by A8, A3, TOPREAL1:def 3

      .= ( LSeg ((f1 /. ( len f1)),(f /. (n + 1)))) by A6, A9, FINSEQ_4: 70

      .= ( LSeg ((f1 /. ( len f1)),(f2 /. 1))) by A10, FINSEQ_5: 27;

      

      thus ( L~ ( Ins (f,n,p))) = ( L~ (g1 ^ f2)) by FINSEQ_5:def 4

      .= ((( L~ g1) \/ ( LSeg ((g1 /. ( len g1)),(f2 /. 1)))) \/ ( L~ f2)) by A10, Th23, RELAT_1: 38

      .= (((( L~ f1) \/ ( LSeg ((f1 /. ( len f1)),p))) \/ ( LSeg ((g1 /. ( len g1)),(f2 /. 1)))) \/ ( L~ f2)) by A9, Th19, RELAT_1: 38

      .= ((( L~ f1) \/ (( LSeg ((f1 /. ( len f1)),p)) \/ ( LSeg ((g1 /. ( len g1)),(f2 /. 1))))) \/ ( L~ f2)) by XBOOLE_1: 4

      .= ((( L~ f1) \/ ( LSeg ((f1 /. ( len f1)),(f2 /. 1)))) \/ ( L~ f2)) by A2, A1, A11, TOPREAL1: 5

      .= ( L~ (f1 ^ f2)) by A7, A10, Th23, RELAT_1: 38

      .= ( L~ f) by RFINSEQ: 8;

    end;

    begin

    registration

      cluster being_S-Seq for FinSequence of ( TOP-REAL 2);

      existence

      proof

        set p = |[ 0 , 0 ]|, q = |[1, 1]|;

        

         A1: (p `2 ) = 0 by EUCLID: 52;

        

         A2: (q `1 ) = 1 by EUCLID: 52;

        

         A3: (q `2 ) = 1 by EUCLID: 52;

        (p `1 ) = 0 by EUCLID: 52;

        then <*p, |[(p `1 ), (q `2 )]|, q*> is being_S-Seq by A1, A2, A3, TOPREAL3: 34;

        hence thesis;

      end;

      cluster being_S-Seq -> one-to-one unfolded s.n.c. special non trivial for FinSequence of ( TOP-REAL 2);

      coherence by NAT_D: 60;

      cluster one-to-one unfolded s.n.c. special non trivial -> being_S-Seq for FinSequence of ( TOP-REAL 2);

      coherence by NAT_D: 60;

      cluster being_S-Seq -> non empty for FinSequence of ( TOP-REAL 2);

      coherence ;

    end

    registration

      cluster one-to-one unfolded s.n.c. special non trivial for FinSequence of ( TOP-REAL 2);

      existence

      proof

        set f = the being_S-Seq FinSequence of ( TOP-REAL 2);

        f is one-to-one unfolded s.n.c. special non trivial;

        hence thesis;

      end;

    end

    theorem :: SPPOL_2:26

    

     Th26: ( len f) <= 2 implies f is unfolded

    proof

      assume

       A1: ( len f) <= 2;

      let i be Nat such that

       A2: 1 <= i;

      assume (i + 2) <= ( len f);

      then (i + 2) <= 2 by A1, XXREAL_0: 2;

      then i <= (2 - 2) by XREAL_1: 19;

      hence thesis by A2, XXREAL_0: 2;

    end;

    

     Lm2: <*p, q*> is unfolded

    proof

      ( len <*p, q*>) = 2 by FINSEQ_1: 44;

      hence thesis by Th26;

    end;

    

     Lm3: f is unfolded implies (f | n) is unfolded

    proof

      assume

       A1: f is unfolded;

      set h = (f | n);

      let i be Nat such that

       A2: 1 <= i and

       A3: (i + 2) <= ( len h);

      

       A4: (i + 1) in ( dom h) by A2, A3, SEQ_4: 135;

      ( len h) <= ( len f) by FINSEQ_5: 16;

      then

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

      

       A6: ((i + 1) + 1) = (i + (1 + 1));

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

      

      hence (( LSeg (h,i)) /\ ( LSeg (h,(i + 1)))) = (( LSeg (f,i)) /\ ( LSeg (h,(i + 1)))) by A3, Th3, XXREAL_0: 2

      .= (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) by A3, A6, Th3

      .= {(f /. (i + 1))} by A1, A2, A5

      .= {(h /. (i + 1))} by A4, FINSEQ_4: 70;

    end;

    

     Lm4: f is unfolded implies (f /^ n) is unfolded

    proof

      assume

       A1: f is unfolded;

      per cases ;

        suppose

         A2: n <= ( len f);

        set h = (f /^ n);

        let i be Nat such that

         A3: 1 <= i and

         A4: (i + 2) <= ( len h);

        

         A5: (i + 1) in ( dom h) by A3, A4, SEQ_4: 135;

        

         A6: ( len h) = (( len f) - n) by A2, RFINSEQ:def 1;

        then (n + (i + 2)) <= ( len f) by A4, XREAL_1: 19;

        then

         A7: ((n + i) + 2) <= ( len f);

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

        then

         A8: 1 <= (n + i) by A3, XXREAL_0: 2;

        

         A9: ((i + 1) + 1) = (i + (1 + 1));

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

        then (i + 1) <= ( len h) by A4, XXREAL_0: 2;

        

        hence (( LSeg (h,i)) /\ ( LSeg (h,(i + 1)))) = (( LSeg (f,(n + i))) /\ ( LSeg (h,(i + 1)))) by A3, A6, Th5

        .= (( LSeg (f,(n + i))) /\ ( LSeg (f,(n + (i + 1))))) by A4, A9, A6, Th5, NAT_1: 11

        .= {(f /. ((n + i) + 1))} by A1, A7, A8

        .= {(f /. (n + (i + 1)))}

        .= {(h /. (i + 1))} by A5, FINSEQ_5: 27;

      end;

        suppose n > ( len f);

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

        then ( len (f /^ n)) = 0 ;

        hence thesis;

      end;

    end;

    registration

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

      cluster (f | n) -> unfolded;

      coherence by Lm3;

      cluster (f /^ n) -> unfolded;

      coherence by Lm4;

    end

    theorem :: SPPOL_2:27

    

     Th27: p in ( rng f) & f is unfolded implies (f :- p) is unfolded

    proof

      assume p in ( rng f);

      then ex i be Element of NAT st (i + 1) = (p .. f) & (f :- p) = (f /^ i) by FINSEQ_5: 49;

      hence thesis;

    end;

    

     Lm5: f is unfolded implies (f -: p) is unfolded

    proof

      (f -: p) = (f | (p .. f)) by FINSEQ_5:def 1;

      hence thesis;

    end;

    registration

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

      cluster (f -: p) -> unfolded;

      coherence by Lm5;

    end

    theorem :: SPPOL_2:28

    

     Th28: f is unfolded implies ( Rev f) is unfolded

    proof

      assume

       A1: f is unfolded;

      

       A2: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

      let i be Nat such that

       A3: 1 <= i and

       A4: (i + 2) <= ( len ( Rev f));

      

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

      then

       A6: (i + 1) in ( dom f) by A3, A4, SEQ_4: 135;

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

      then

      reconsider j9 = (( len f) - (i + 1)) as Element of NAT by A4, A5, INT_1: 5, XXREAL_0: 2;

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

      then

      reconsider j = (( len f) - i) as Element of NAT by A4, A5, INT_1: 5, XXREAL_0: 2;

      

       A7: (j9 + (i + 1)) = ( len f);

      i in ( dom f) by A3, A4, A5, SEQ_4: 135;

      then (j + 1) in ( dom f) by A2, FINSEQ_5: 2;

      then

       A8: (j9 + 2) <= ( len f) by FINSEQ_3: 25;

      

       A9: (j + (i + 1)) = (( len f) + 1);

      (i + (1 + 1)) = ((i + 1) + 1);

      then

       A10: 1 <= j9 by A4, A5, XREAL_1: 19;

      (j + i) = ( len f);

      

      hence (( LSeg (( Rev f),i)) /\ ( LSeg (( Rev f),(i + 1)))) = (( LSeg (f,j)) /\ ( LSeg (( Rev f),(i + 1)))) by Th2

      .= (( LSeg (f,(j9 + 1))) /\ ( LSeg (f,j9))) by A7, Th2

      .= {(f /. (j9 + 1))} by A1, A10, A8

      .= {(( Rev f) /. (i + 1))} by A9, A2, A6, FINSEQ_5: 2, FINSEQ_5: 66;

    end;

    theorem :: SPPOL_2:29

    

     Th29: g is unfolded & (( LSeg (p,(g /. 1))) /\ ( LSeg (g,1))) = {(g /. 1)} implies ( <*p*> ^ g) is unfolded

    proof

      set f = <*p*>;

      

       A1: ( len f) = 1 by FINSEQ_1: 39;

      

       A2: (f /. 1) = p by FINSEQ_4: 16;

      

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

      assume that

       A4: g is unfolded and

       A5: (( LSeg (p,(g /. 1))) /\ ( LSeg (g,1))) = {(g /. 1)};

      let i be Nat such that

       A6: 1 <= i and

       A7: (i + 2) <= ( len (f ^ g));

      

       A8: (i + (1 + 1)) = ((i + 1) + 1);

      per cases ;

        suppose

         A9: i = ( len f);

        then

         A10: ( LSeg ((f ^ g),(i + 1))) = ( LSeg (g,1)) by Th7;

        now

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

          then

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

          assume ( len g) = 0 ;

          hence contradiction by A1, A6, A7, A3, A11, XXREAL_0: 2;

        end;

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

        then

         A12: 1 in ( dom g) by FINSEQ_3: 25;

        then ( LSeg ((f ^ g),i)) = ( LSeg ((f /. ( len f)),(g /. 1))) by A9, Th8, RELAT_1: 38;

        hence thesis by A1, A5, A2, A9, A12, A10, FINSEQ_4: 69;

      end;

        suppose

         A13: i <> ( len f);

        reconsider j = (i - ( len f)) as Element of NAT by A1, A6, INT_1: 5;

        i > ( len f) by A1, A6, A13, XXREAL_0: 1;

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

        then

         A14: 1 <= j by XREAL_1: 19;

        

         A15: ((i + 2) - ( len f)) <= ( len g) by A7, A3, XREAL_1: 20;

        then

         A16: (j + (1 + 1)) <= ( len g);

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

        then (j + 1) <= ( len g) by A15, XXREAL_0: 2;

        then

         A17: (j + 1) in ( dom g) by A14, SEQ_4: 134;

        

         A18: (( len f) + (j + 1)) = (i + 1);

        (( len f) + j) = i;

        

        hence (( LSeg ((f ^ g),i)) /\ ( LSeg ((f ^ g),(i + 1)))) = (( LSeg (g,j)) /\ ( LSeg ((f ^ g),(i + 1)))) by A14, Th7

        .= (( LSeg (g,j)) /\ ( LSeg (g,(j + 1)))) by A18, Th7, NAT_1: 11

        .= {(g /. (j + 1))} by A4, A14, A16

        .= {((f ^ g) /. (i + 1))} by A18, A17, FINSEQ_4: 69;

      end;

    end;

    theorem :: SPPOL_2:30

    

     Th30: f is unfolded & (k + 1) = ( len f) & (( LSeg (f,k)) /\ ( LSeg ((f /. ( len f)),p))) = {(f /. ( len f))} implies (f ^ <*p*>) is unfolded

    proof

      set g = <*p*>;

      assume that

       A1: f is unfolded and

       A2: (k + 1) = ( len f) and

       A3: (( LSeg (f,k)) /\ ( LSeg ((f /. ( len f)),p))) = {(f /. ( len f))};

      

       A4: ( len g) = 1 by FINSEQ_1: 39;

      

       A5: (g /. 1) = p by FINSEQ_4: 16;

      

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

      let i be Nat such that

       A7: 1 <= i and

       A8: (i + 2) <= ( len (f ^ g));

      

       A9: (i + (1 + 1)) = ((i + 1) + 1);

      per cases ;

        suppose

         A10: (i + 2) <= ( len f);

        then

         A11: (i + 1) in ( dom f) by A7, SEQ_4: 135;

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

        

        hence (( LSeg ((f ^ g),i)) /\ ( LSeg ((f ^ g),(i + 1)))) = (( LSeg (f,i)) /\ ( LSeg ((f ^ g),(i + 1)))) by A10, Th6, XXREAL_0: 2

        .= (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) by A9, A10, Th6

        .= {(f /. (i + 1))} by A1, A7, A10

        .= {((f ^ g) /. (i + 1))} by A11, FINSEQ_4: 68;

      end;

        suppose (i + 2) > ( len f);

        then

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

        

         A13: f is non empty by A4, A8, A6, A9, XREAL_1: 6;

        then

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

        (i + 1) <= ( len f) by A4, A8, A6, A9, XREAL_1: 6;

        then

         A15: (i + 1) = ( len f) by A12, XXREAL_0: 1;

        then

         A16: ( LSeg ((f ^ g),(i + 1))) = ( LSeg ((f /. ( len f)),(g /. 1))) by A13, Th8;

        ( LSeg ((f ^ g),i)) = ( LSeg (f,k)) by A2, A15, Th6;

        hence thesis by A3, A5, A15, A16, A14, FINSEQ_4: 68;

      end;

    end;

    theorem :: SPPOL_2:31

    

     Th31: f is unfolded & g is unfolded & (k + 1) = ( len f) & (( LSeg (f,k)) /\ ( LSeg ((f /. ( len f)),(g /. 1)))) = {(f /. ( len f))} & (( LSeg ((f /. ( len f)),(g /. 1))) /\ ( LSeg (g,1))) = {(g /. 1)} implies (f ^ g) is unfolded

    proof

      assume that

       A1: f is unfolded and

       A2: g is unfolded and

       A3: (k + 1) = ( len f) and

       A4: (( LSeg (f,k)) /\ ( LSeg ((f /. ( len f)),(g /. 1)))) = {(f /. ( len f))} and

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

      let i be Nat such that

       A6: 1 <= i and

       A7: (i + 2) <= ( len (f ^ g));

      

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

      per cases ;

        suppose

         A9: (i + 2) <= ( len f);

        then

         A10: (i + 1) in ( dom f) by A6, SEQ_4: 135;

        

         A11: (i + (1 + 1)) = ((i + 1) + 1);

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

        

        hence (( LSeg ((f ^ g),i)) /\ ( LSeg ((f ^ g),(i + 1)))) = (( LSeg (f,i)) /\ ( LSeg ((f ^ g),(i + 1)))) by A9, Th6, XXREAL_0: 2

        .= (( LSeg (f,i)) /\ ( LSeg (f,(i + 1)))) by A9, A11, Th6

        .= {(f /. (i + 1))} by A1, A6, A9

        .= {((f ^ g) /. (i + 1))} by A10, FINSEQ_4: 68;

      end;

        suppose

         A12: (i + 2) > ( len f);

        

         A13: (i + (1 + 1)) = ((i + 1) + 1);

        now

          per cases ;

            suppose

             A14: i <= ( len f);

            ( len g) <> 0 by A7, A8, A12;

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

            then

             A15: 1 in ( dom g) by FINSEQ_3: 25;

            

             A16: f is non empty by A6, A14;

            now

              per cases ;

                suppose

                 A17: i = ( len f);

                then

                 A18: ( LSeg ((f ^ g),(i + 1))) = ( LSeg (g,1)) by Th7;

                ( LSeg ((f ^ g),i)) = ( LSeg ((f /. ( len f)),(g /. 1))) by A16, A15, A17, Th8, RELAT_1: 38;

                hence thesis by A5, A15, A17, A18, FINSEQ_4: 69;

              end;

                suppose i <> ( len f);

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

                then

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

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

                then

                 A20: (i + 1) = ( len f) by A19, XXREAL_0: 1;

                then

                 A21: ( LSeg ((f ^ g),i)) = ( LSeg (f,k)) by A3, Th6;

                

                 A22: ( len f) in ( dom f) by A16, FINSEQ_5: 6;

                ( LSeg ((f ^ g),(i + 1))) = ( LSeg ((f /. ( len f)),(g /. 1))) by A16, A15, A20, Th8, RELAT_1: 38;

                hence thesis by A4, A20, A21, A22, FINSEQ_4: 68;

              end;

            end;

            hence thesis;

          end;

            suppose

             A23: i > ( len f);

            then

            reconsider j = (i - ( len f)) as Element of NAT by INT_1: 5;

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

            then

             A24: 1 <= j by XREAL_1: 19;

            

             A25: ((i + 2) - ( len f)) <= ( len g) by A7, A8, XREAL_1: 20;

            then

             A26: (j + (1 + 1)) <= ( len g);

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

            then (j + 1) <= ( len g) by A25, XXREAL_0: 2;

            then

             A27: (j + 1) in ( dom g) by A24, SEQ_4: 134;

            

             A28: (( len f) + (j + 1)) = (i + 1);

            (( len f) + j) = i;

            

            hence (( LSeg ((f ^ g),i)) /\ ( LSeg ((f ^ g),(i + 1)))) = (( LSeg (g,j)) /\ ( LSeg ((f ^ g),(i + 1)))) by A24, Th7

            .= (( LSeg (g,j)) /\ ( LSeg (g,(j + 1)))) by A28, Th7, NAT_1: 11

            .= {(g /. (j + 1))} by A2, A24, A26

            .= {((f ^ g) /. (i + 1))} by A28, A27, FINSEQ_4: 69;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: SPPOL_2:32

    

     Th32: f is unfolded & p in ( LSeg (f,n)) implies ( Ins (f,n,p)) is unfolded

    proof

      assume that

       A1: f is unfolded and

       A2: p in ( LSeg (f,n));

      set f1 = (f | n), g1 = (f1 ^ <*p*>), f2 = (f /^ n);

      

       A3: (n + 1) <= ( len f) by A2, TOPREAL1:def 3;

      

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

      then

       A5: ( len f1) = n by A3, FINSEQ_1: 59, XXREAL_0: 2;

      then

       A6: (n + 1) = ( len g1) by FINSEQ_2: 16;

      

       A7: n <= ( len f) by A3, A4, XXREAL_0: 2;

      1 <= (( len f) - n) by A3, XREAL_1: 19;

      then

       A8: 1 <= ( len f2) by A7, RFINSEQ:def 1;

      then

       ZZ: 1 in ( dom f2) by FINSEQ_3: 25;

      then

       A9: (f /. (n + 1)) = (f2 /. 1) by FINSEQ_5: 27;

      

       A10: 1 <= n by A2, TOPREAL1:def 3;

      then

       A11: ( LSeg (f,n)) = ( LSeg ((f /. n),(f /. (n + 1)))) by A3, TOPREAL1:def 3;

      

       A12: n in ( dom f1) by A10, A5, FINSEQ_3: 25;

      then

       A13: (f /. n) = (f1 /. ( len f1)) by A5, FINSEQ_4: 70;

      

       A14: (g1 /. ( len g1)) = (g1 /. (( len f1) + 1)) by FINSEQ_2: 16

      .= p by FINSEQ_4: 67;

      then

       A15: (( LSeg ((f1 /. ( len f1)),p)) \/ ( LSeg ((g1 /. ( len g1)),(f2 /. 1)))) = ( LSeg ((f1 /. ( len f1)),(f2 /. 1))) by A2, A11, A13, A9, TOPREAL1: 5;

       A16:

      now

        ( len f1) <> 0 by A2, A5, TOPREAL1:def 3;

        then

        consider k be Nat such that

         A17: (k + 1) = ( len f1) by NAT_1: 6;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        

         A18: (k + (1 + 1)) <= ( len f) by A3, A5, A17;

        per cases ;

          suppose k <> 0 ;

          then

           A19: 1 <= k by NAT_1: 14;

          ( LSeg (f1,k)) = ( LSeg (f,k)) by A17, Th3;

          then

           A20: (( LSeg (f1,k)) /\ ( LSeg (f,n))) = {(f /. n)} by A1, A5, A17, A18, A19;

          now

            let x be object;

            hereby

              assume

               A21: x in (( LSeg (f1,k)) /\ ( LSeg ((f1 /. ( len f1)),p)));

              then x in ( LSeg ((f1 /. ( len f1)),p)) by XBOOLE_0:def 4;

              then

               A22: x in ( LSeg (f,n)) by A11, A13, A9, A15, XBOOLE_0:def 3;

              x in ( LSeg (f1,k)) by A21, XBOOLE_0:def 4;

              then x in (( LSeg (f1,k)) /\ ( LSeg (f,n))) by A22, XBOOLE_0:def 4;

              hence x = (f /. n) by A20, TARSKI:def 1;

            end;

            assume

             A23: x = (f /. n);

            then x in (( LSeg (f1,k)) /\ ( LSeg (f,n))) by A20, TARSKI:def 1;

            then

             A24: x in ( LSeg (f1,k)) by XBOOLE_0:def 4;

            x in ( LSeg ((f1 /. ( len f1)),p)) by A13, A23, RLTOPSP1: 68;

            hence x in (( LSeg (f1,k)) /\ ( LSeg ((f1 /. ( len f1)),p))) by A24, XBOOLE_0:def 4;

          end;

          then (( LSeg (f1,k)) /\ ( LSeg ((f1 /. ( len f1)),p))) = {(f1 /. ( len f1))} by A13, TARSKI:def 1;

          hence g1 is unfolded by A1, A17, Th30;

        end;

          suppose k = 0 ;

          then ( len g1) = (1 + 1) by A17, FINSEQ_2: 16;

          hence g1 is unfolded by Th26;

        end;

      end;

      (f1 /. ( len f1)) = (g1 /. n) by A5, A12, FINSEQ_4: 68;

      then ( LSeg (g1,n)) = ( LSeg ((f1 /. ( len f1)),(g1 /. ( len g1)))) by A10, A6, TOPREAL1:def 3;

      then

       A25: (( LSeg (g1,n)) /\ ( LSeg ((g1 /. ( len g1)),(f2 /. 1)))) = {(g1 /. ( len g1))} by A2, A14, A11, A13, A9, TOPREAL1: 8;

      now

        per cases ;

          suppose ( len f2) = 1;

          

          then f2 = <*(f2 . 1)*> by FINSEQ_5: 14

          .= <*(f2 /. 1)*> by ZZ, PARTFUN1:def 6;

          hence (g1 ^ f2) is unfolded by A16, A6, A25, Th30;

        end;

          suppose ( len f2) <> 1;

          then ( len f2) > 1 by A8, XXREAL_0: 1;

          then

           A26: (1 + 1) <= ( len f2) by NAT_1: 13;

          then ( LSeg (f2,1)) = ( LSeg ((f2 /. 1),(f2 /. (1 + 1)))) by TOPREAL1:def 3;

          then

           A27: (f2 /. 1) in ( LSeg (f2,1)) by RLTOPSP1: 68;

          

           A28: (1 + 1) <= (( len f) - n) by A7, A26, RFINSEQ:def 1;

          then (n + (1 + 1)) <= ( len f) by XREAL_1: 19;

          

          then

           A29: {(f /. (n + 1))} = (( LSeg (f,n)) /\ ( LSeg (f,(n + 1)))) by A1, A10

          .= (( LSeg (f,n)) /\ ( LSeg (f2,1))) by A28, Th5;

          now

            let x be object;

            hereby

              assume

               A30: x in (( LSeg ((g1 /. ( len g1)),(f2 /. 1))) /\ ( LSeg (f2,1)));

              then x in ( LSeg ((g1 /. ( len g1)),(f2 /. 1))) by XBOOLE_0:def 4;

              then

               A31: x in ( LSeg (f,n)) by A11, A13, A9, A15, XBOOLE_0:def 3;

              x in ( LSeg (f2,1)) by A30, XBOOLE_0:def 4;

              then x in (( LSeg (f,n)) /\ ( LSeg (f2,1))) by A31, XBOOLE_0:def 4;

              hence x = (f2 /. 1) by A9, A29, TARSKI:def 1;

            end;

            assume

             A32: x = (f2 /. 1);

            then x in ( LSeg ((g1 /. ( len g1)),(f2 /. 1))) by RLTOPSP1: 68;

            hence x in (( LSeg ((g1 /. ( len g1)),(f2 /. 1))) /\ ( LSeg (f2,1))) by A27, A32, XBOOLE_0:def 4;

          end;

          then (( LSeg ((g1 /. ( len g1)),(f2 /. 1))) /\ ( LSeg (f2,1))) = {(f2 /. 1)} by TARSKI:def 1;

          hence (g1 ^ f2) is unfolded by A1, A16, A6, A25, Th31;

        end;

      end;

      hence thesis by FINSEQ_5:def 4;

    end;

    theorem :: SPPOL_2:33

    

     Th33: ( len f) <= 2 implies f is s.n.c.

    proof

      assume

       A1: ( len f) <= 2;

      let i,j be Nat such that

       A2: (i + 1) < j;

      now

        assume that

         A3: 1 <= i and

         A4: (i + 1) <= ( len f) and

         A5: 1 <= j and

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

        (j + 1) <= (1 + 1) by A1, A6, XXREAL_0: 2;

        then j <= 1 by XREAL_1: 6;

        then

         A7: j = 1 by A5, XXREAL_0: 1;

        (i + 1) <= (1 + 1) by A1, A4, XXREAL_0: 2;

        then i <= 1 by XREAL_1: 6;

        then i = 1 by A3, XXREAL_0: 1;

        hence contradiction by A2, A7;

      end;

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

      hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

    end;

    

     Lm6: <*p, q*> is s.n.c.

    proof

      ( len <*p, q*>) = 2 by FINSEQ_1: 44;

      hence thesis by Th33;

    end;

    

     Lm7: f is s.n.c. implies (f | n) is s.n.c.

    proof

      assume

       A1: f is s.n.c.;

      let i,j be Nat such that

       A2: (i + 1) < j;

      per cases ;

        suppose

         A3: i = 0 or (j + 1) > ( len (f | n));

        now

          per cases by A3;

            case i = 0 ;

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

          end;

            case (j + 1) > ( len (f | n));

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

          end;

        end;

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

        hence thesis;

      end;

        suppose that i <> 0 and

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

        

         A5: ( LSeg (f,i)) misses ( LSeg (f,j)) by A1, A2;

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

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

        

        then (( LSeg ((f | n),i)) /\ ( LSeg ((f | n),j))) = (( LSeg (f,i)) /\ ( LSeg ((f | n),j))) by A4, Th3, XXREAL_0: 2

        .= {} by A5, A4, Th3;

        hence thesis;

      end;

    end;

    

     Lm8: f is s.n.c. implies (f /^ n) is s.n.c.

    proof

      assume

       A1: f is s.n.c.;

      per cases ;

        suppose

         A2: n <= ( len f);

        let i,j be Nat such that

         A3: (i + 1) < j;

        now

          per cases ;

            suppose

             A4: i = 0 or (j + 1) > ( len (f /^ n));

            now

              per cases by A4;

                case i = 0 ;

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

              end;

                case (j + 1) > ( len (f /^ n));

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

              end;

            end;

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

            hence thesis;

          end;

            suppose that

             A5: i <> 0 and

             A6: (j + 1) <= ( len (f /^ n));

            

             A7: i <= j by A3, NAT_1: 13;

            1 <= i by A5, NAT_1: 14;

            then

             A8: 1 <= j by A7, XXREAL_0: 2;

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

            then ((n + i) + 1) < (n + j);

            then

             A9: ( LSeg (f,(n + i))) misses ( LSeg (f,(n + j))) by A1;

            

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

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

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

            then (i + 1) <= ( len (f /^ n)) by A6, XXREAL_0: 2;

            

            then (( LSeg ((f /^ n),i)) /\ ( LSeg ((f /^ n),j))) = (( LSeg (f,(n + i))) /\ ( LSeg ((f /^ n),j))) by A5, A10, Th5, NAT_1: 14

            .= {} by A9, A6, A10, A8, Th5;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

        suppose n > ( len f);

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

        then ( len (f /^ n)) = 0 ;

        hence thesis by Th33;

      end;

    end;

    registration

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

      cluster (f | n) -> s.n.c.;

      coherence by Lm7;

      cluster (f /^ n) -> s.n.c.;

      coherence by Lm8;

    end

    

     Lm9: f is s.n.c. implies (f -: p) is s.n.c.

    proof

      (f -: p) = (f | (p .. f)) by FINSEQ_5:def 1;

      hence thesis;

    end;

    registration

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

      cluster (f -: p) -> s.n.c.;

      coherence by Lm9;

    end

    theorem :: SPPOL_2:34

    

     Th34: p in ( rng f) & f is s.n.c. implies (f :- p) is s.n.c.

    proof

      assume p in ( rng f);

      then ex i be Element of NAT st (i + 1) = (p .. f) & (f :- p) = (f /^ i) by FINSEQ_5: 49;

      hence thesis;

    end;

    theorem :: SPPOL_2:35

    

     Th35: f is s.n.c. implies ( Rev f) is s.n.c.

    proof

      assume

       A1: f is s.n.c.;

      let i,j be Nat such that

       A2: (i + 1) < j;

      per cases ;

        suppose

         A3: i = 0 or (j + 1) > ( len ( Rev f));

        now

          per cases by A3;

            case i = 0 ;

            hence ( LSeg (( Rev f),i)) = {} by TOPREAL1:def 3;

          end;

            case (j + 1) > ( len ( Rev f));

            hence ( LSeg (( Rev f),j)) = {} by TOPREAL1:def 3;

          end;

        end;

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

        hence thesis;

      end;

        suppose that i <> 0 and

         A4: (j + 1) <= ( len ( Rev f));

        

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

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

        then

         A6: i < j by A2, XXREAL_0: 2;

        

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

        then

        reconsider j9 = (( len f) - j) as Element of NAT by A4, A5, INT_1: 5, XXREAL_0: 2;

        j <= ( len f) by A4, A7, A5, XXREAL_0: 2;

        then

        reconsider i9 = (( len f) - i) as Element of NAT by A6, INT_1: 5, XXREAL_0: 2;

        

         A8: (j9 + j) = ( len f);

        (( len f) - (i + 1)) > j9 by A2, XREAL_1: 10;

        then ((i9 - 1) + 1) > (j9 + 1) by XREAL_1: 6;

        then

         A9: ( LSeg (f,i9)) misses ( LSeg (f,j9)) by A1;

        (i9 + i) = ( len f);

        

        hence (( LSeg (( Rev f),i)) /\ ( LSeg (( Rev f),j))) = (( LSeg (f,i9)) /\ ( LSeg (( Rev f),j))) by Th2

        .= {} by A9, A8, Th2;

      end;

    end;

    theorem :: SPPOL_2:36

    

     Th36: f is s.n.c. & g is s.n.c. & ( L~ f) misses ( L~ g) & (for i st 1 <= i & (i + 2) <= ( len f) holds ( LSeg (f,i)) misses ( LSeg ((f /. ( len f)),(g /. 1)))) & (for i st 2 <= i & (i + 1) <= ( len g) holds ( LSeg (g,i)) misses ( LSeg ((f /. ( len f)),(g /. 1)))) implies (f ^ g) is s.n.c.

    proof

      assume that

       A1: f is s.n.c. and

       A2: g is s.n.c. and

       A3: (( L~ f) /\ ( L~ g)) = {} and

       A4: for i st 1 <= i & (i + 2) <= ( len f) holds ( LSeg (f,i)) misses ( LSeg ((f /. ( len f)),(g /. 1))) and

       A5: for i st 2 <= i & (i + 1) <= ( len g) holds ( LSeg (g,i)) misses ( LSeg ((f /. ( len f)),(g /. 1)));

      let i,j be Nat such that

       A6: (i + 1) < j;

      per cases ;

        suppose

         A7: i = 0 or (j + 1) > ( len (f ^ g));

        now

          per cases by A7;

            case i = 0 ;

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

          end;

            case (j + 1) > ( len (f ^ g));

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

          end;

        end;

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

        hence thesis;

      end;

        suppose that

         A8: i <> 0 and

         A9: (j + 1) <= ( len (f ^ g));

        

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

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

        then

         A11: i < j by A6, XXREAL_0: 2;

        

         A12: 1 <= i by A8, NAT_1: 14;

        now

          per cases ;

            suppose

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

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

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

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

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

            then

             A14: ( LSeg ((f ^ g),i)) = ( LSeg (f,i)) by Th6;

            ( LSeg ((f ^ g),j)) = ( LSeg (f,j)) by A13, Th6;

            hence thesis by A1, A6, A14;

          end;

            suppose (j + 1) > ( len f);

            then

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

            then

            reconsider j9 = (j - ( len f)) as Element of NAT by INT_1: 5;

            ((j + 1) - ( len f)) <= ( len g) by A9, A10, XREAL_1: 20;

            then

             A16: (j9 + 1) <= ( len g);

            

             A17: (( len f) + j9) = j;

            now

              per cases ;

                suppose

                 A18: i <= ( len f);

                then

                 A19: f is non empty by A12;

                now

                  per cases ;

                    suppose

                     A20: i = ( len f);

                    g is non empty by A16;

                    then

                     A21: ( LSeg ((f ^ g),i)) = ( LSeg ((f /. ( len f)),(g /. 1))) by A19, A20, Th8;

                    ((( len f) + 1) + 1) <= j by A6, A20, NAT_1: 13;

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

                    then

                     A22: (1 + 1) <= j9 by XREAL_1: 19;

                    then ( LSeg ((f ^ g),j)) = ( LSeg (g,j9)) by A17, Th7, XXREAL_0: 2;

                    hence thesis by A5, A16, A22, A21;

                  end;

                    suppose i <> ( len f);

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

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

                    then

                     A23: ( LSeg ((f ^ g),i)) = ( LSeg (f,i)) by Th6;

                    now

                      per cases ;

                        suppose

                         A24: j = ( len f);

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

                        then

                         A25: (i + (1 + 1)) <= ( len f);

                        g is non empty by A9, A10, A24, XREAL_1: 6;

                        then

                         A26: ( LSeg ((f ^ g),j)) = ( LSeg ((f /. ( len f)),(g /. 1))) by A19, A24, Th8;

                        thus thesis by A4, A8, A23, A25, A26, NAT_1: 14;

                      end;

                        suppose j <> ( len f);

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

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

                        then 1 <= j9 by XREAL_1: 19;

                        then ( LSeg ((f ^ g),(( len f) + j9))) = ( LSeg (g,j9)) by Th7;

                        then

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

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

                        then (( LSeg ((f ^ g),i)) /\ ( LSeg ((f ^ g),j))) = {} by A3, A27, XBOOLE_1: 3, XBOOLE_1: 27;

                        hence thesis;

                      end;

                    end;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A28: i > ( len f);

                then j <> ( len f) by A6, NAT_1: 13;

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

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

                then 1 <= j9 by XREAL_1: 19;

                then

                 A29: ( LSeg ((f ^ g),(( len f) + j9))) = ( LSeg (g,j9)) by Th7;

                reconsider i9 = (i - ( len f)) as Element of NAT by A28, INT_1: 5;

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

                then 1 <= i9 by XREAL_1: 19;

                then

                 A30: ( LSeg ((f ^ g),(( len f) + i9))) = ( LSeg (g,i9)) by Th7;

                ((i + 1) - ( len f)) < j9 by A6, XREAL_1: 9;

                then (i9 + 1) < j9;

                hence thesis by A2, A30, A29;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: SPPOL_2:37

    

     Th37: f is unfolded s.n.c. & p in ( LSeg (f,n)) & not p in ( rng f) implies ( Ins (f,n,p)) is s.n.c.

    proof

      assume that

       A1: f is unfolded and

       A2: f is s.n.c. and

       A3: p in ( LSeg (f,n)) and

       A4: not p in ( rng f);

      set fp = ( Ins (f,n,p));

      let i,j be Nat such that

       A5: (i + 1) < j;

      per cases ;

        suppose

         A6: i = 0 or (j + 1) > ( len fp);

        now

          per cases by A6;

            case i = 0 ;

            hence ( LSeg (fp,i)) = {} by TOPREAL1:def 3;

          end;

            case (j + 1) > ( len fp);

            hence ( LSeg (fp,j)) = {} by TOPREAL1:def 3;

          end;

        end;

        then (( LSeg (fp,i)) /\ ( LSeg (fp,j))) = {} ;

        hence thesis;

      end;

        suppose that

         A7: i <> 0 and

         A8: (j + 1) <= ( len fp);

        

         A9: 1 <= i by A7, NAT_1: 14;

        set f1 = (f | n), g1 = (f1 ^ <*p*>), f2 = (f /^ n);

        

         A10: fp = (g1 ^ f2) by FINSEQ_5:def 4;

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

        then

         A11: i < j by A5, XXREAL_0: 2;

        

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

        

         A13: ( len fp) = (( len f) + 1) by FINSEQ_5: 69;

        

         A14: 1 <= n by A3, TOPREAL1:def 3;

        

         A15: (n + 1) <= ( len f) by A3, TOPREAL1:def 3;

        

         A16: ( len g1) = (( len f1) + 1) by FINSEQ_2: 16;

        then

         A17: (g1 /. ( len g1)) = p by FINSEQ_4: 67;

        

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

        then

         A19: n <= ( len f) by A15, XXREAL_0: 2;

        

         A20: ( len f1) = n by A15, A18, FINSEQ_1: 59, XXREAL_0: 2;

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

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

        then

         A21: (((i + 1) + 1) + 1) <= (( len f) + 1) by A8, A13, XXREAL_0: 2;

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

        then

         A22: (i + 1) <= ( len f) by A12, XXREAL_0: 2;

        now

          per cases ;

            suppose

             A23: (j + 1) <= n;

            

            then

             A24: ( LSeg (fp,j)) = ( LSeg (g1,j)) by A10, A16, A18, A20, Th6, XXREAL_0: 2

            .= ( LSeg (f1,j)) by A20, A23, Th6

            .= ( LSeg (f,j)) by A20, A23, Th3;

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

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

            then i < n by A23, XXREAL_0: 2;

            then

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

            

            then ( LSeg (fp,i)) = ( LSeg (g1,i)) by A10, A16, A18, A20, Th6, XXREAL_0: 2

            .= ( LSeg (f1,i)) by A20, A25, Th6

            .= ( LSeg (f,i)) by A20, A25, Th3;

            hence thesis by A2, A5, A24;

          end;

            suppose (j + 1) > n;

            then

             A26: n <= j by NAT_1: 13;

            now

              per cases ;

                suppose

                 A27: i <= (n + 1);

                

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

                1 <= (( len f) - n) by A15, XREAL_1: 19;

                then 1 <= ( len f2) by A19, RFINSEQ:def 1;

                then 1 in ( dom f2) by FINSEQ_3: 25;

                then

                 A29: (f /. (n + 1)) = (f2 /. 1) by FINSEQ_5: 27;

                ( len g1) in ( dom g1) by FINSEQ_5: 6;

                then

                 A30: (fp /. (n + 1)) = (g1 /. ( len g1)) by A10, A16, A20, FINSEQ_4: 68;

                

                 Z1: (n + 1) in ( dom f) by A15, A28, FINSEQ_3: 25;

                

                 Z2: ((n + 1) + 1) >= 1 by NAT_1: 11;

                ((n + 1) + 1) <= (( len f) + 1) by A15, XREAL_1: 6;

                then ((n + 1) + 1) <= ( len fp) by A13;

                then ((n + 1) + 1) in ( dom fp) by Z2, FINSEQ_3: 25;

                

                then

                 A31: (fp /. ((n + 1) + 1)) = (fp . ((n + 1) + 1)) by PARTFUN1:def 6

                .= (f . (n + 1)) by A15, FINSEQ_5: 74

                .= (f /. (n + 1)) by Z1, PARTFUN1:def 6;

                

                 A32: n in ( dom f1) by A14, A20, FINSEQ_3: 25;

                then

                 A33: (f /. n) = (f1 /. ( len f1)) by A20, FINSEQ_4: 70;

                ((n + 1) + 1) <= ( len fp) by A13, A15, XREAL_1: 6;

                then

                 A34: ( LSeg (fp,(n + 1))) = ( LSeg (p,(f2 /. 1))) by A17, A29, A31, A28, A30, TOPREAL1:def 3;

                

                 A35: (f1 /. ( len f1)) = (g1 /. ( len f1)) by A20, A32, FINSEQ_4: 68;

                

                 A36: ( LSeg (fp,n)) = ( LSeg (g1,n)) by A10, A16, A20, Th6

                .= ( LSeg ((f1 /. ( len f1)),p)) by A16, A17, A14, A20, A35, TOPREAL1:def 3;

                

                 A37: ( LSeg (f,n)) = ( LSeg ((f /. n),(f /. (n + 1)))) by A14, A15, TOPREAL1:def 3;

                then

                 A38: (( LSeg ((f1 /. ( len f1)),p)) \/ ( LSeg ((g1 /. ( len g1)),(f2 /. 1)))) = ( LSeg ((f1 /. ( len f1)),(f2 /. 1))) by A3, A17, A33, A29, TOPREAL1: 5;

                

                 A39: (( LSeg ((f1 /. ( len f1)),p)) /\ ( LSeg (p,(f2 /. 1)))) = {p} by A3, A37, A33, A29, TOPREAL1: 8;

                now

                  per cases by XXREAL_0: 1;

                    suppose i < n;

                    then

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

                    

                    then

                     A41: ( LSeg (fp,i)) = ( LSeg (g1,i)) by A10, A16, A18, A20, Th6, XXREAL_0: 2

                    .= ( LSeg (f1,i)) by A20, A40, Th6

                    .= ( LSeg (f,i)) by A20, A40, Th3;

                    now

                      per cases ;

                        suppose

                         A42: j = n;

                        then

                         A43: ( LSeg (f,i)) misses ( LSeg (f,n)) by A2, A5;

                        (( LSeg (fp,i)) /\ ( LSeg (fp,j))) c= (( LSeg (f,i)) /\ ( LSeg (f,n))) by A37, A33, A29, A38, A36, A41, A42, XBOOLE_1: 7, XBOOLE_1: 26;

                        then (( LSeg (fp,i)) /\ ( LSeg (fp,j))) c= {} by A43;

                        then (( LSeg (fp,i)) /\ ( LSeg (fp,j))) = {} by XBOOLE_1: 3;

                        hence thesis;

                      end;

                        suppose j <> n;

                        then n < j by A26, XXREAL_0: 1;

                        then

                         A44: (n + 1) <= j by NAT_1: 13;

                        now

                          per cases ;

                            suppose

                             A45: j = (n + 1);

                            now

                              per cases ;

                                suppose

                                 A46: (i + 1) = n;

                                

                                 A47: (i + (1 + 1)) <= ( len f) by A21, XREAL_1: 6;

                                ( LSeg (fp,i)) = ( LSeg (g1,i)) by A10, A16, A20, A46, Th6, NAT_1: 11

                                .= ( LSeg (f1,i)) by A20, A46, Th6

                                .= ( LSeg (f,i)) by A20, A46, Th3;

                                then

                                 A48: (( LSeg (fp,i)) /\ ( LSeg (f,n))) = {(f /. n)} by A1, A9, A46, A47;

                                assume not thesis;

                                then

                                consider x be object such that

                                 A49: x in (( LSeg (fp,i)) /\ ( LSeg (fp,j))) by XBOOLE_0: 4;

                                

                                 A50: x in ( LSeg (fp,i)) by A49, XBOOLE_0:def 4;

                                

                                 A51: x in ( LSeg (fp,j)) by A49, XBOOLE_0:def 4;

                                then x in ( LSeg (f,n)) by A17, A37, A33, A29, A38, A34, A45, XBOOLE_0:def 3;

                                then x in {(f /. n)} by A48, A50, XBOOLE_0:def 4;

                                then

                                 A52: x = (f /. n) by TARSKI:def 1;

                                then x in ( LSeg (fp,n)) by A33, A36, RLTOPSP1: 68;

                                then x in (( LSeg (fp,n)) /\ ( LSeg (fp,(n + 1)))) by A45, A51, XBOOLE_0:def 4;

                                then

                                 A53: p = (f /. n) by A36, A34, A39, A52, TARSKI:def 1;

                                n in ( dom f) by A14, A15, SEQ_4: 134;

                                hence contradiction by A4, A53, PARTFUN2: 2;

                              end;

                                suppose (i + 1) <> n;

                                then (i + 1) < n by A40, XXREAL_0: 1;

                                then

                                 A54: ( LSeg (f,i)) misses ( LSeg (f,n)) by A2;

                                (( LSeg (fp,i)) /\ ( LSeg (fp,j))) c= (( LSeg (f,i)) /\ ( LSeg (f,n))) by A17, A37, A33, A29, A38, A34, A41, A45, XBOOLE_1: 7, XBOOLE_1: 26;

                                then (( LSeg (fp,i)) /\ ( LSeg (fp,j))) c= {} by A54;

                                then (( LSeg (fp,i)) /\ ( LSeg (fp,j))) = {} by XBOOLE_1: 3;

                                hence thesis;

                              end;

                            end;

                            hence thesis;

                          end;

                            suppose

                             A55: j <> (n + 1);

                            reconsider nj = (j - (n + 1)) as Element of NAT by A44, INT_1: 5;

                            

                             A56: (n + 1) < j by A44, A55, XXREAL_0: 1;

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

                            then

                             A57: 1 <= nj by XREAL_1: 19;

                            reconsider j9 = (j - 1) as Element of NAT by A9, A11, INT_1: 5, XXREAL_0: 2;

                            

                             A58: (n + nj) = j9;

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

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

                            then

                             A59: (i + 1) < j9 by XREAL_1: 20;

                            j = (nj + (n + 1));

                            

                            then ( LSeg (fp,j)) = ( LSeg (f2,nj)) by A10, A16, A20, A57, Th7

                            .= ( LSeg (f,j9)) by A19, A57, A58, Th4;

                            hence thesis by A2, A41, A59;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    hence thesis;

                  end;

                    suppose

                     A60: i = n;

                    then

                    reconsider nj = (j - (n + 1)) as Element of NAT by A5, INT_1: 5;

                    

                     A61: ((n + 1) + 1) <= j by A5, A60, NAT_1: 13;

                    then

                     A62: 1 <= nj by XREAL_1: 19;

                    reconsider j9 = (j - 1) as Element of NAT by A9, A11, INT_1: 5, XXREAL_0: 2;

                    

                     A63: (n + nj) = j9;

                    j = (nj + (n + 1));

                    

                    then

                     A64: ( LSeg (fp,j)) = ( LSeg (f2,nj)) by A10, A16, A20, A62, Th7

                    .= ( LSeg (f,j9)) by A19, A62, A63, Th4;

                    now

                      per cases ;

                        suppose j <> ((n + 1) + 1);

                        then ((n + 1) + 1) < j by A61, XXREAL_0: 1;

                        then (i + 1) < j9 by A60, XREAL_1: 20;

                        then

                         A65: ( LSeg (f,i)) misses ( LSeg (f,j9)) by A2;

                        (( LSeg (fp,i)) /\ ( LSeg (fp,j))) c= (( LSeg (f,i)) /\ ( LSeg (f,j9))) by A37, A33, A29, A38, A36, A60, A64, XBOOLE_1: 7, XBOOLE_1: 26;

                        then (( LSeg (fp,i)) /\ ( LSeg (fp,j))) c= {} by A65;

                        then (( LSeg (fp,i)) /\ ( LSeg (fp,j))) = {} by XBOOLE_1: 3;

                        hence thesis;

                      end;

                        suppose

                         A66: j = ((n + 1) + 1);

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

                        then

                         A67: (( LSeg (f,n)) /\ ( LSeg (f,j9))) = {(f /. j9)} by A1, A14, A66;

                        assume not thesis;

                        then

                        consider x be object such that

                         A68: x in (( LSeg (fp,i)) /\ ( LSeg (fp,j))) by XBOOLE_0: 4;

                        

                         A69: x in ( LSeg (fp,j)) by A68, XBOOLE_0:def 4;

                        

                         A70: x in ( LSeg (fp,i)) by A68, XBOOLE_0:def 4;

                        then x in ( LSeg (f,n)) by A37, A33, A29, A38, A36, A60, XBOOLE_0:def 3;

                        then x in {(f /. (n + 1))} by A64, A66, A67, A69, XBOOLE_0:def 4;

                        then

                         A71: x = (f /. (n + 1)) by TARSKI:def 1;

                        then x in ( LSeg (fp,(n + 1))) by A29, A34, RLTOPSP1: 68;

                        then x in (( LSeg (fp,n)) /\ ( LSeg (fp,(n + 1)))) by A60, A70, XBOOLE_0:def 4;

                        then

                         A72: p = (f /. (n + 1)) by A36, A34, A39, A71, TARSKI:def 1;

                        (n + 1) in ( dom f) by A14, A15, SEQ_4: 134;

                        hence contradiction by A4, A72, PARTFUN2: 2;

                      end;

                    end;

                    hence thesis;

                  end;

                    suppose

                     A73: i > n;

                    reconsider j9 = (j - 1) as Element of NAT by A9, A11, INT_1: 5, XXREAL_0: 2;

                    i >= (n + 1) by A73, NAT_1: 13;

                    then

                     A74: i = (n + 1) by A27, XXREAL_0: 1;

                    then (n + 1) < j9 by A5, XREAL_1: 20;

                    then

                     A75: ( LSeg (f,n)) misses ( LSeg (f,j9)) by A2;

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

                    then

                    reconsider nj = (j - (n + 1)) as Element of NAT by A5, A74, INT_1: 5, XXREAL_0: 2;

                    

                     A76: 1 <= nj by A5, A74, XREAL_1: 19;

                    

                     A77: (n + nj) = j9;

                    j = (nj + (n + 1));

                    

                    then ( LSeg (fp,j)) = ( LSeg (f2,nj)) by A10, A16, A20, A76, Th7

                    .= ( LSeg (f,j9)) by A19, A76, A77, Th4;

                    then (( LSeg (fp,(n + 1))) /\ ( LSeg (fp,j))) c= (( LSeg (f,n)) /\ ( LSeg (f,j9))) by A17, A37, A33, A29, A38, A34, XBOOLE_1: 7, XBOOLE_1: 26;

                    then (( LSeg (fp,(n + 1))) /\ ( LSeg (fp,j))) c= {} by A75;

                    then (( LSeg (fp,(n + 1))) /\ ( LSeg (fp,j))) = {} by XBOOLE_1: 3;

                    hence thesis by A74;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A78: i > (n + 1);

                then

                reconsider nj = (j - (n + 1)) as Element of NAT by A11, INT_1: 5, XXREAL_0: 2;

                (n + 1) < j by A11, A78, XXREAL_0: 2;

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

                then

                 A79: 1 <= nj by XREAL_1: 19;

                reconsider ni = (i - (n + 1)) as Element of NAT by A78, INT_1: 5;

                ((n + 1) + 1) <= i by A78, NAT_1: 13;

                then

                 A80: 1 <= ni by XREAL_1: 19;

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

                then (i + 1) <= (( len f) + 1) by A22, XXREAL_0: 2;

                then ((i + 1) - (n + 1)) <= ((( len f) + 1) - (n + 1)) by XREAL_1: 9;

                then

                 A81: (ni + 1) <= (( len f) - n);

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

                reconsider j9 = (j - 1) as Element of NAT by A9, A11, INT_1: 5, XXREAL_0: 2;

                

                 A82: (n + ni) = i9;

                ((i + 1) - 1) < j9 by A5, XREAL_1: 9;

                then

                 A83: (i9 + 1) < j9;

                

                 A84: (n + nj) = j9;

                j = (nj + (n + 1));

                

                then

                 A85: ( LSeg (fp,j)) = ( LSeg (f2,nj)) by A10, A16, A20, A79, Th7

                .= ( LSeg (f,j9)) by A19, A79, A84, Th4;

                i = (ni + (n + 1));

                

                then ( LSeg (fp,i)) = ( LSeg (f2,ni)) by A10, A16, A20, A80, Th7

                .= ( LSeg (f,i9)) by A80, A81, A82, Th5;

                hence thesis by A2, A83, A85;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end;

    registration

      cluster ( <*> the carrier of ( TOP-REAL 2)) -> special;

      coherence ;

    end

    registration

      let p;

      cluster <*p*> -> special;

      coherence

      proof

        set f = <*p*>;

        f is special

        proof

          let i be Nat such that

           A1: 1 <= i and

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

          ( len f) = ( 0 + 1) by FINSEQ_1: 39;

          hence thesis by A1, A2, XREAL_1: 6;

        end;

        hence thesis;

      end;

    end

    theorem :: SPPOL_2:38

    

     Th38: (p `1 ) = (q `1 ) or (p `2 ) = (q `2 ) implies <*p, q*> is special

    proof

      assume

       A1: (p `1 ) = (q `1 ) or (p `2 ) = (q `2 );

      set f = <*p, q*>;

      let i be Nat such that

       A2: 1 <= i and

       A3: (i + 1) <= ( len f);

      ( len f) = (1 + 1) by FINSEQ_1: 44;

      then i <= 1 by A3, XREAL_1: 6;

      then

       A4: i = 1 by A2, XXREAL_0: 1;

      then (f /. i) = p by FINSEQ_4: 17;

      hence thesis by A1, A4, FINSEQ_4: 17;

    end;

    

     Lm10: f is special implies (f | n) is special

    proof

      assume

       A1: f is special;

      let i be Nat such that

       A2: 1 <= i and

       A3: (i + 1) <= ( len (f | n));

      i in ( dom (f | n)) by A2, A3, SEQ_4: 134;

      then

       A4: ((f | n) /. i) = (f /. i) by FINSEQ_4: 70;

      (i + 1) in ( dom (f | n)) by A2, A3, SEQ_4: 134;

      then

       A5: ((f | n) /. (i + 1)) = (f /. (i + 1)) by FINSEQ_4: 70;

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

      then (i + 1) <= ( len f) by A3, XXREAL_0: 2;

      hence thesis by A1, A2, A4, A5;

    end;

    

     Lm11: f is special implies (f /^ n) is special

    proof

      assume

       A1: f is special;

      per cases ;

        suppose

         A2: n <= ( len f);

        let i be Nat such that

         A3: 1 <= i and

         A4: (i + 1) <= ( len (f /^ n));

        i in ( dom (f /^ n)) by A3, A4, SEQ_4: 134;

        then

         A5: ((f /^ n) /. i) = (f /. (n + i)) by FINSEQ_5: 27;

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

        then

         A6: 1 <= (n + i) by A3, XXREAL_0: 2;

        (i + 1) in ( dom (f /^ n)) by A3, A4, SEQ_4: 134;

        

        then

         A7: ((f /^ n) /. (i + 1)) = (f /. (n + (i + 1))) by FINSEQ_5: 27

        .= (f /. ((n + i) + 1));

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

        then (n + (i + 1)) <= ( len f) by A4, XREAL_1: 19;

        hence thesis by A1, A5, A7, A6;

      end;

        suppose n > ( len f);

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

        hence thesis;

      end;

    end;

    registration

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

      cluster (f | n) -> special;

      coherence by Lm10;

      cluster (f /^ n) -> special;

      coherence by Lm11;

    end

    theorem :: SPPOL_2:39

    

     Th39: p in ( rng f) & f is special implies (f :- p) is special

    proof

      assume p in ( rng f);

      then ex i be Element of NAT st (i + 1) = (p .. f) & (f :- p) = (f /^ i) by FINSEQ_5: 49;

      hence thesis;

    end;

    

     Lm12: f is special implies (f -: p) is special

    proof

      (f -: p) = (f | (p .. f)) by FINSEQ_5:def 1;

      hence thesis;

    end;

    registration

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

      cluster (f -: p) -> special;

      coherence by Lm12;

    end

    theorem :: SPPOL_2:40

    

     Th40: f is special implies ( Rev f) is special

    proof

      assume

       A1: f is special;

      

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

      let i be Nat such that

       A3: 1 <= i and

       A4: (i + 1) <= ( len ( Rev f));

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

      then

      reconsider j = (( len f) - i) as Element of NAT by A4, A2, INT_1: 5, XXREAL_0: 2;

      j <= (( len f) - 1) by A3, XREAL_1: 10;

      then

       A5: (j + 1) <= ((( len f) - 1) + 1) by XREAL_1: 6;

      

       A6: ((1 + i) + j) = (( len f) + 1);

      

       A7: ((i + 1) - i) <= j by A4, A2, XREAL_1: 9;

      then j in ( dom f) by A5, SEQ_4: 134;

      then

       A8: (( Rev f) /. (i + 1)) = (f /. j) by A6, FINSEQ_5: 66;

      

       A9: (i + (j + 1)) = (( len f) + 1);

      (j + 1) in ( dom f) by A5, A7, SEQ_4: 134;

      then (( Rev f) /. i) = (f /. (j + 1)) by A9, FINSEQ_5: 66;

      hence thesis by A1, A5, A7, A8;

    end;

    

     Lm13: f is special & g is special & (((f /. ( len f)) `1 ) = ((g /. 1) `1 ) or ((f /. ( len f)) `2 ) = ((g /. 1) `2 )) implies (f ^ g) is special

    proof

      assume that

       A1: f is special and

       A2: g is special and

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

      let i be Nat such that

       A4: 1 <= i and

       A5: (i + 1) <= ( len (f ^ g));

      

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

      per cases by XXREAL_0: 1;

        suppose i < ( len f);

        then

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

        then (i + 1) in ( dom f) by A4, SEQ_4: 134;

        then

         A8: ((f ^ g) /. (i + 1)) = (f /. (i + 1)) by FINSEQ_4: 68;

        i in ( dom f) by A4, A7, SEQ_4: 134;

        then ((f ^ g) /. i) = (f /. i) by FINSEQ_4: 68;

        hence thesis by A1, A4, A7, A8;

      end;

        suppose

         A9: i = ( len f);

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

        then

         A10: ((f ^ g) /. i) = (f /. i) by FINSEQ_4: 68;

        1 <= ( len g) by A5, A6, A9, XREAL_1: 6;

        then 1 in ( dom g) by FINSEQ_3: 25;

        hence thesis by A3, A9, A10, FINSEQ_4: 69;

      end;

        suppose

         A11: i > ( len f);

        then

        reconsider j = (i - ( len f)) as Element of NAT by INT_1: 5;

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

        then

         A12: 1 <= j by XREAL_1: 19;

        

         A13: (( len f) + (j + 1)) = (i + 1);

        

         A14: ((i + 1) - ( len f)) <= ( len g) by A5, A6, XREAL_1: 20;

        then (j + 1) in ( dom g) by A12, SEQ_4: 134;

        then

         A15: ((f ^ g) /. (i + 1)) = (g /. (j + 1)) by A13, FINSEQ_4: 69;

        

         A16: (( len f) + j) = i;

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

        then j in ( dom g) by A12, SEQ_4: 134;

        then ((f ^ g) /. i) = (g /. j) by A16, FINSEQ_4: 69;

        hence thesis by A2, A12, A14, A15;

      end;

    end;

    theorem :: SPPOL_2:41

    

     Th41: f is special & p in ( LSeg (f,n)) implies ( Ins (f,n,p)) is special

    proof

      assume that

       A1: f is special and

       A2: p in ( LSeg (f,n));

      

       A3: (n + 1) <= ( len f) by A2, TOPREAL1:def 3;

      then

       A4: 1 <= (( len f) - n) by XREAL_1: 19;

      

       A5: 1 <= n by A2, TOPREAL1:def 3;

      then

       A6: ( LSeg (f,n)) = ( LSeg ((f /. n),(f /. (n + 1)))) by A3, TOPREAL1:def 3;

      set f1 = (f | n), g1 = (f1 ^ <*p*>), f2 = (f /^ n);

      set p1 = (f1 /. ( len f1)), p2 = (f2 /. 1);

      

       A7: p1 = |[(p1 `1 ), (p1 `2 )]| by EUCLID: 53;

      

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

      then n <= ( len f) by A3, XXREAL_0: 2;

      then 1 <= ( len f2) by A4, RFINSEQ:def 1;

      then 1 in ( dom f2) by FINSEQ_3: 25;

      then

       A9: (f /. (n + 1)) = (f2 /. 1) by FINSEQ_5: 27;

      

       A10: ( len f1) = n by A3, A8, FINSEQ_1: 59, XXREAL_0: 2;

      then n in ( dom f1) by A5, FINSEQ_3: 25;

      then

       A11: (f /. n) = (f1 /. ( len f1)) by A10, FINSEQ_4: 70;

      then

       A12: (p1 `1 ) = (p2 `1 ) or (p1 `2 ) = (p2 `2 ) by A1, A5, A3, A9;

      set q1 = (g1 /. ( len g1));

      

       A13: p2 = |[(p2 `1 ), (p2 `2 )]| by EUCLID: 53;

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

      then (p1 `1 ) = (( <*p*> /. 1) `1 ) or (p1 `2 ) = (( <*p*> /. 1) `2 ) by A2, A6, A11, A9, A12, A7, A13, TOPREAL3: 11, TOPREAL3: 12;

      then

       A14: g1 is special by A1, Lm13;

      (g1 /. ( len g1)) = (g1 /. (( len f1) + 1)) by FINSEQ_2: 16

      .= p by FINSEQ_4: 67;

      then (q1 `1 ) = (p2 `1 ) or (q1 `2 ) = (p2 `2 ) by A2, A6, A11, A9, A12, A7, A13, TOPREAL3: 11, TOPREAL3: 12;

      then (g1 ^ f2) is special by A1, A14, Lm13;

      hence thesis by FINSEQ_5:def 4;

    end;

    theorem :: SPPOL_2:42

    

     Th42: q in ( rng f) & 1 <> (q .. f) & (q .. f) <> ( len f) & f is unfolded s.n.c. implies (( L~ (f -: q)) /\ ( L~ (f :- q))) = {q}

    proof

      assume that

       A1: q in ( rng f) and

       A2: 1 <> (q .. f) and

       A3: (q .. f) <> ( len f) and

       A4: f is unfolded and

       A5: f is s.n.c.;

      

       A6: ((f :- q) /. 1) = q by FINSEQ_5: 53;

      (q .. f) <= ( len f) by A1, FINSEQ_4: 21;

      then (q .. f) < ( len f) by A3, XXREAL_0: 1;

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

      then

       A7: 1 <= (( len f) - (q .. f)) by XREAL_1: 19;

      ( len (f :- q)) = ((( len f) - (q .. f)) + 1) by A1, FINSEQ_5: 50;

      then (1 + 1) <= ( len (f :- q)) by A7, XREAL_1: 6;

      then

       A8: ( rng (f :- q)) c= ( L~ (f :- q)) by Th18;

      1 in ( dom (f :- q)) by FINSEQ_5: 6;

      then

       A9: q in ( rng (f :- q)) by A6, PARTFUN2: 2;

      (f -: q) is non empty by A1, FINSEQ_5: 47;

      then

       A10: ( len (f -: q)) in ( dom (f -: q)) by FINSEQ_5: 6;

      

       A11: ( len (f -: q)) = (q .. f) by A1, FINSEQ_5: 42;

      thus (( L~ (f -: q)) /\ ( L~ (f :- q))) c= {q}

      proof

        let x be object;

        assume

         A12: x in (( L~ (f -: q)) /\ ( L~ (f :- q)));

        then

        reconsider p = x as Point of ( TOP-REAL 2);

        p in ( L~ (f -: q)) by A12, XBOOLE_0:def 4;

        then

        consider i such that

         A13: 1 <= i and

         A14: (i + 1) <= ( len (f -: q)) and

         A15: p in ( LSeg ((f -: q),i)) by Th13;

        

         A16: ( LSeg ((f -: q),i)) = ( LSeg (f,i)) by A14, Th9;

        p in ( L~ (f :- q)) by A12, XBOOLE_0:def 4;

        then

        consider j such that

         A17: 1 <= j and (j + 1) <= ( len (f :- q)) and

         A18: p in ( LSeg ((f :- q),j)) by Th13;

        consider j9 be Nat such that

         A19: j = (j9 + 1) by A17, NAT_1: 6;

        reconsider j9 as Element of NAT by ORDINAL1:def 12;

        

         A20: ( LSeg ((f :- q),j)) = ( LSeg (f,(j9 + (q .. f)))) by A1, A19, Th10;

        per cases ;

          suppose that

           A21: (i + 1) = ( len (f -: q)) and

           A22: j9 = 0 ;

          (q .. f) <= ( len f) by A1, FINSEQ_4: 21;

          then (q .. f) < ( len f) by A3, XXREAL_0: 1;

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

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

          

          then (( LSeg ((f -: q),i)) /\ ( LSeg ((f :- q),j))) = {(f /. (q .. f))} by A4, A11, A13, A16, A20, A21, A22

          .= {q} by A1, FINSEQ_5: 38;

          hence thesis by A15, A18, XBOOLE_0:def 4;

        end;

          suppose that

           A23: (i + 1) = ( len (f -: q)) and

           A24: j9 <> 0 ;

          1 <= j9 by A24, NAT_1: 14;

          then ((i + 1) + 1) <= (j9 + (q .. f)) by A11, A23, XREAL_1: 7;

          then (i + 1) < (j9 + (q .. f)) by NAT_1: 13;

          then ( LSeg ((f -: q),i)) misses ( LSeg ((f :- q),j)) by A5, A16, A20;

          then (( LSeg ((f -: q),i)) /\ ( LSeg ((f :- q),j))) = {} ;

          hence thesis by A15, A18, XBOOLE_0:def 4;

        end;

          suppose

           A25: (i + 1) <> ( len (f -: q));

          

           A26: (q .. f) <= (j9 + (q .. f)) by NAT_1: 11;

          (i + 1) < (q .. f) by A11, A14, A25, XXREAL_0: 1;

          then (i + 1) < (j9 + (q .. f)) by A26, XXREAL_0: 2;

          then ( LSeg ((f -: q),i)) misses ( LSeg ((f :- q),j)) by A5, A16, A20;

          then (( LSeg ((f -: q),i)) /\ ( LSeg ((f :- q),j))) = {} ;

          hence thesis by A15, A18, XBOOLE_0:def 4;

        end;

      end;

      1 <= (q .. f) by A1, FINSEQ_4: 21;

      then 1 < (q .. f) by A2, XXREAL_0: 1;

      then (1 + 1) <= (q .. f) by NAT_1: 13;

      then

       A27: ( rng (f -: q)) c= ( L~ (f -: q)) by A11, Th18;

      ((f -: q) /. (q .. f)) = q by A1, FINSEQ_5: 45;

      then q in ( rng (f -: q)) by A11, A10, PARTFUN2: 2;

      then q in (( L~ (f -: q)) /\ ( L~ (f :- q))) by A27, A9, A8, XBOOLE_0:def 4;

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: SPPOL_2:43

    

     Th43: p <> q & ((p `1 ) = (q `1 ) or (p `2 ) = (q `2 )) implies <*p, q*> is being_S-Seq by FINSEQ_3: 94, FINSEQ_1: 44, Lm2, Lm6, Th38;

    definition

      mode S-Sequence_in_R2 is being_S-Seq FinSequence of ( TOP-REAL 2);

    end

    registration

      let f be S-Sequence_in_R2;

      cluster ( Rev f) -> being_S-Seq;

      coherence

      proof

        set g = ( Rev f);

        g is being_S-Seq

        proof

          thus g is one-to-one;

          ( len g) = ( len f) by FINSEQ_5:def 3;

          hence ( len g) >= 2 by TOPREAL1:def 8;

          thus thesis by Th28, Th35, Th40;

        end;

        hence thesis;

      end;

    end

    theorem :: SPPOL_2:44

    for f be S-Sequence_in_R2 st i in ( dom f) holds (f /. i) in ( L~ f)

    proof

      let f be S-Sequence_in_R2;

      ( len f) >= 2 by TOPREAL1:def 8;

      hence thesis by GOBOARD1: 1;

    end;

    theorem :: SPPOL_2:45

    p <> q & ((p `1 ) = (q `1 ) or (p `2 ) = (q `2 )) implies ( LSeg (p,q)) is being_S-P_arc

    proof

      assume that

       A1: p <> q and

       A2: (p `1 ) = (q `1 ) or (p `2 ) = (q `2 );

      take f = <*p, q*>;

      thus f is being_S-Seq by A1, A2, Th43;

      thus thesis by Th21;

    end;

    

     Lm14: p in ( rng f) implies ( L~ (f -: p)) c= ( L~ f)

    proof

      assume p in ( rng f);

      then ( L~ f) = (( L~ (f -: p)) \/ ( L~ (f :- p))) by Th24;

      hence thesis by XBOOLE_1: 7;

    end;

    

     Lm15: p in ( rng f) implies ( L~ (f :- p)) c= ( L~ f)

    proof

      assume p in ( rng f);

      then ( L~ f) = (( L~ (f -: p)) \/ ( L~ (f :- p))) by Th24;

      hence thesis by XBOOLE_1: 7;

    end;

    theorem :: SPPOL_2:46

    

     Th46: for f be S-Sequence_in_R2 st p in ( rng f) & (p .. f) <> 1 holds (f -: p) is being_S-Seq

    proof

      let f be S-Sequence_in_R2 such that

       A1: p in ( rng f) and

       A2: (p .. f) <> 1;

      thus (f -: p) is one-to-one;

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

      then 1 < (p .. f) by A2, XXREAL_0: 1;

      then (1 + 1) <= (p .. f) by NAT_1: 13;

      hence ( len (f -: p)) >= 2 by A1, FINSEQ_5: 42;

      thus thesis;

    end;

    theorem :: SPPOL_2:47

    for f be S-Sequence_in_R2 st p in ( rng f) & (p .. f) <> ( len f) holds (f :- p) is being_S-Seq

    proof

      let f be S-Sequence_in_R2 such that

       A1: p in ( rng f) and

       A2: (p .. f) <> ( len f);

      thus (f :- p) is one-to-one by A1, FINSEQ_5: 56;

      hereby

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

        then (p .. f) < ( len f) by A2, XXREAL_0: 1;

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

        then

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

        assume ( len (f :- p)) < 2;

        then ((( len f) - (p .. f)) + 1) < (1 + 1) by A1, FINSEQ_5: 50;

        hence contradiction by A3, XREAL_1: 6;

      end;

      thus thesis by A1, Th27, Th34, Th39;

    end;

    theorem :: SPPOL_2:48

    

     Th48: for f be S-Sequence_in_R2 st p in ( LSeg (f,i)) & not p in ( rng f) holds ( Ins (f,i,p)) is being_S-Seq

    proof

      let f be S-Sequence_in_R2 such that

       A1: p in ( LSeg (f,i)) and

       A2: not p in ( rng f);

      set g = ( Ins (f,i,p));

      thus g is one-to-one by A2, FINSEQ_5: 76;

      ( len g) = (( len f) + 1) by FINSEQ_5: 69;

      then

       A3: ( len g) >= ( len f) by NAT_1: 11;

      ( len f) >= 2 by TOPREAL1:def 8;

      hence ( len g) >= 2 by A3, XXREAL_0: 2;

      thus g is unfolded by A1, Th32;

      thus g is s.n.c. by A1, A2, Th37;

      thus thesis by A1, Th41;

    end;

    begin

    registration

      cluster being_S-P_arc for Subset of ( TOP-REAL 2);

      existence

      proof

        set p = |[ 0 , 0 ]|, q = |[1, 1]|, f = <*p, |[(p `1 ), (q `2 )]|, q*>;

        

         A1: (p `2 ) = 0 by EUCLID: 52;

        

         A2: (q `1 ) = 1 by EUCLID: 52;

        

         A3: (q `2 ) = 1 by EUCLID: 52;

        (p `1 ) = 0 by EUCLID: 52;

        then f is being_S-Seq by A1, A2, A3, TOPREAL3: 34;

        then ( L~ f) is being_S-P_arc;

        hence thesis;

      end;

    end

    theorem :: SPPOL_2:49

    P is_S-P_arc_joining (p1,p2) implies P is_S-P_arc_joining (p2,p1)

    proof

      given f such that

       A1: f is being_S-Seq and

       A2: P = ( L~ f) and

       A3: p1 = (f /. 1) and

       A4: p2 = (f /. ( len f));

      take g = ( Rev f);

      thus g is being_S-Seq & P = ( L~ g) by A1, A2, Th22;

      ( len g) = ( len f) by FINSEQ_5:def 3;

      hence thesis by A1, A3, A4, FINSEQ_5: 65;

    end;

    definition

      let p1, p2;

      let P be Subset of ( TOP-REAL 2);

      :: SPPOL_2:def1

      pred p1,p2 split P means p1 <> p2 & ex f1,f2 be S-Sequence_in_R2 st p1 = (f1 /. 1) & p1 = (f2 /. 1) & p2 = (f1 /. ( len f1)) & p2 = (f2 /. ( len f2)) & (( L~ f1) /\ ( L~ f2)) = {p1, p2} & P = (( L~ f1) \/ ( L~ f2));

    end

    theorem :: SPPOL_2:50

    

     Th50: (p1,p2) split P implies (p2,p1) split P

    proof

      assume

       A1: p1 <> p2;

      given f1,f2 be S-Sequence_in_R2 such that

       A2: p1 = (f1 /. 1) and

       A3: p1 = (f2 /. 1) and

       A4: p2 = (f1 /. ( len f1)) and

       A5: p2 = (f2 /. ( len f2)) and

       A6: (( L~ f1) /\ ( L~ f2)) = {p1, p2} and

       A7: P = (( L~ f1) \/ ( L~ f2));

      thus p2 <> p1 by A1;

      reconsider g1 = ( Rev f1), g2 = ( Rev f2) as S-Sequence_in_R2;

      take g1, g2;

      

       A8: ( len g2) = ( len f2) by FINSEQ_5:def 3;

      ( len g1) = ( len f1) by FINSEQ_5:def 3;

      hence p2 = (g1 /. 1) & p2 = (g2 /. 1) & p1 = (g1 /. ( len g1)) & p1 = (g2 /. ( len g2)) by A2, A3, A4, A5, A8, FINSEQ_5: 65;

      ( L~ g1) = ( L~ f1) by Th22;

      hence thesis by A6, A7, Th22;

    end;

    

     Lm16: for f1,f2 be S-Sequence_in_R2 st p1 = (f1 /. 1) & p1 = (f2 /. 1) & p2 = (f1 /. ( len f1)) & p2 = (f2 /. ( len f2)) & (( L~ f1) /\ ( L~ f2)) = {p1, p2} & P = (( L~ f1) \/ ( L~ f2)) & q <> p1 & q in ( rng f1) holds ex g1,g2 be S-Sequence_in_R2 st p1 = (g1 /. 1) & p1 = (g2 /. 1) & q = (g1 /. ( len g1)) & q = (g2 /. ( len g2)) & (( L~ g1) /\ ( L~ g2)) = {p1, q} & P = (( L~ g1) \/ ( L~ g2))

    proof

      let f1,f2 be S-Sequence_in_R2 such that

       A1: p1 = (f1 /. 1) and

       A2: p1 = (f2 /. 1) and

       A3: p2 = (f1 /. ( len f1)) and

       A4: p2 = (f2 /. ( len f2)) and

       A5: (( L~ f1) /\ ( L~ f2)) = {p1, p2} and

       A6: P = (( L~ f1) \/ ( L~ f2)) and

       A7: q <> p1 and

       A8: q in ( rng f1);

      set f19 = ( Rev (f1 :- q));

      

       A9: 1 <= (q .. f1) by A8, FINSEQ_4: 21;

       A10:

      now

        assume

         A11: 1 = (q .. f1);

        then

         A12: 1 in ( dom f1) by A8, FINSEQ_4: 20;

        (f1 . 1) = q by A8, A11, FINSEQ_4: 19;

        hence contradiction by A1, A7, A12, PARTFUN1:def 6;

      end;

      then

      reconsider g1 = (f1 -: q) as S-Sequence_in_R2 by A8, Th46;

      

       A13: 1 in ( dom g1) by FINSEQ_5: 6;

      1 in ( dom f2) by FINSEQ_5: 6;

      then 1 <= ( len f2) by FINSEQ_3: 25;

      then

      reconsider l = (( len f2) - 1) as Element of NAT by INT_1: 5;

      set f29 = (f2 | l);

      

       A14: (l + 1) = ( len f2);

      ( rng f19) = ( rng (f1 :- q)) by FINSEQ_5: 57;

      then

       A15: ( rng f19) c= ( rng f1) by A8, FINSEQ_5: 55;

      ( len f2) >= 2 by TOPREAL1:def 8;

      then

       A16: ( rng f2) c= ( L~ f2) by Th18;

      ( len f1) >= 2 by TOPREAL1:def 8;

      then ( rng f1) c= ( L~ f1) by Th18;

      then

       A17: (( rng f2) /\ ( rng f1)) c= (( L~ f1) /\ ( L~ f2)) by A16, XBOOLE_1: 27;

      set g2 = (f29 ^ f19);

      

       A18: ( dom f29) = ( Seg ( len f29)) by FINSEQ_1:def 3;

      ( len (f1 :- q)) >= 1 by NAT_1: 14;

      then

       A19: ( len f19) >= 1 by FINSEQ_5:def 3;

      then

       A20: ( len f19) in ( dom f19) & 1 in ( dom f19) by FINSEQ_3: 25;

      

       A21: l < ( len f2) by XREAL_1: 44;

      then

       A22: ( len f29) = l by FINSEQ_1: 59;

      ( len f2) >= 2 by TOPREAL1:def 8;

      then

       A23: (( len f2) - 1) >= ((1 + 1) - 1) by XREAL_1: 9;

      then

       A24: l in ( dom f29) by A22, FINSEQ_3: 25;

      then

       A25: (f29 /. ( len f29)) = (f2 /. l) by A22, FINSEQ_4: 70;

      

       A26: (f19 /. 1) = ((f1 :- q) /. ( len (f1 :- q))) by FINSEQ_5: 65

      .= (f2 /. ( len f2)) by A3, A4, A8, FINSEQ_5: 54;

      then

       A27: ( LSeg ((f29 /. ( len f29)),(f19 /. 1))) = ( LSeg (f2,l)) by A23, A14, A25, TOPREAL1:def 3;

       A28:

      now

        let i such that 1 <= i and

         A29: (i + 2) <= ( len f29);

        ((i + 1) + 1) <= ( len f29) by A29;

        then

         A30: (i + 1) < ( len f29) by NAT_1: 13;

        then ( LSeg (f29,i)) = ( LSeg (f2,i)) by Th3;

        hence ( LSeg (f29,i)) misses ( LSeg ((f29 /. ( len f29)),(f19 /. 1))) by A22, A27, A30, TOPREAL1:def 7;

      end;

      

       A31: 1 in ( dom f1) by FINSEQ_5: 6;

       A32:

      now

        

         A33: (1 + 1) <= ( len f1) by TOPREAL1:def 8;

        p1 in ( LSeg ((f1 /. 1),(f1 /. (1 + 1)))) by A1, RLTOPSP1: 68;

        then

         A34: p1 in ( LSeg (f1,1)) by A33, TOPREAL1:def 3;

        assume p1 in ( L~ f19);

        then

         A35: p1 in ( L~ (f1 :- q)) by Th22;

        then

        consider i such that

         A36: 1 <= i and (i + 1) <= ( len (f1 :- q)) and

         A37: p1 in ( LSeg ((f1 :- q),i)) by Th13;

        consider j be Nat such that

         A38: i = (j + 1) by A36, NAT_1: 6;

        

         A39: 1 < (q .. f1) by A10, A9, XXREAL_0: 1;

        reconsider j as Element of NAT by ORDINAL1:def 12;

        

         A40: ( LSeg ((f1 :- q),i)) = ( LSeg (f1,(j + (q .. f1)))) by A8, A38, Th10;

        then p1 in (( LSeg (f1,1)) /\ ( LSeg (f1,(j + (q .. f1))))) by A37, A34, XBOOLE_0:def 4;

        then

         A41: ( LSeg (f1,1)) meets ( LSeg (f1,(j + (q .. f1))));

        per cases ;

          suppose

           A42: j = 0 ;

          

           A43: (1 + 1) <= (q .. f1) by A39, NAT_1: 13;

          now

            per cases by A43, XXREAL_0: 1;

              suppose

               A44: (q .. f1) = 2;

              

               A45: (q .. f1) <= ( len f1) by A8, FINSEQ_4: 21;

              now

                per cases by A44, A45, XXREAL_0: 1;

                  suppose ( len f1) = 2;

                  then ( len (f1 :- q)) = ((( len f1) - ( len f1)) + 1) by A8, A44, FINSEQ_5: 50;

                  hence contradiction by A35, TOPREAL1: 22;

                end;

                  suppose ( len f1) > 2;

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

                  then (( LSeg (f1,1)) /\ ( LSeg (f1,(1 + 1)))) = {(f1 /. (1 + 1))} by TOPREAL1:def 6;

                  then p1 in {(f1 /. 2)} by A37, A34, A40, A42, A44, XBOOLE_0:def 4;

                  then

                   A46: p1 = (f1 /. 2) by TARSKI:def 1;

                  2 in ( dom f1) by A8, A44, FINSEQ_4: 20;

                  hence contradiction by A1, A31, A46, PARTFUN2: 10;

                end;

              end;

              hence contradiction;

            end;

              suppose (q .. f1) > 2;

              then (1 + 1) < (j + (q .. f1)) by A42;

              hence contradiction by A41, TOPREAL1:def 7;

            end;

          end;

          hence contradiction;

        end;

          suppose j <> 0 ;

          then (1 + 1) < (j + (q .. f1)) by A39, NAT_1: 14, XREAL_1: 8;

          hence contradiction by A41, TOPREAL1:def 7;

        end;

      end;

       A47:

      now

        let i such that

         A48: 2 <= i and

         A49: (i + 1) <= ( len f19);

        reconsider m = (( len f19) - (i + 1)) as Element of NAT by A49, INT_1: 5;

        ((m + 1) + i) = ( len (f1 :- q)) by FINSEQ_5:def 3;

        

        then

         A50: ( LSeg (f19,i)) = ( LSeg ((f1 :- q),(m + 1))) by Th2

        .= ( LSeg (f1,(m + (q .. f1)))) by A8, Th10;

        then

         A51: ( LSeg (f19,i)) c= ( L~ f1) by TOPREAL3: 19;

         A52:

        now

          

           A53: ( len f1) >= (1 + 1) by TOPREAL1:def 8;

          then

          reconsider k = (( len f1) - 1) as Element of NAT by INT_1: 5, XXREAL_0: 2;

          

           A54: p2 in ( LSeg ((f1 /. k),(f1 /. ( len f1)))) by A3, RLTOPSP1: 68;

          

           A55: (k + 1) = ( len f1);

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

          then

           A56: p2 in ( LSeg (f1,k)) by A55, A54, TOPREAL1:def 3;

          

           A57: ( len f19) = ( len (f1 :- q)) by FINSEQ_5:def 3;

          

           A58: (( len f1) - i) = (((((( len f1) - (q .. f1)) + 1) - 1) + (q .. f1)) - i)

          .= (((( len f19) - 1) + (q .. f1)) - i) by A8, A57, FINSEQ_5: 50

          .= (m + (q .. f1));

          per cases ;

            suppose

             A59: i = (1 + 1);

            

             A60: (q .. f1) <= (m + (q .. f1)) by NAT_1: 11;

            1 <= (q .. f1) by A8, FINSEQ_4: 21;

            then

             A61: 1 <= (m + (q .. f1)) by A60, XXREAL_0: 2;

            assume

             A62: p2 in ( LSeg (f19,i));

            

             A63: ((m + (q .. f1)) + (1 + 1)) = ( len f1) by A58, A59;

            

             A64: 1 <= k by A53, XREAL_1: 19;

            p2 in ( LSeg ((f1 /. k),(f1 /. (k + 1)))) by A3, RLTOPSP1: 68;

            then

             A65: p2 in ( LSeg (f1,k)) by A64, TOPREAL1:def 3;

            ((m + (q .. f1)) + 1) = k by A58, A59;

            then (( LSeg (f1,(m + (q .. f1)))) /\ ( LSeg (f1,k))) = {(f1 /. k)} by A61, A63, TOPREAL1:def 6;

            then p2 in {(f1 /. k)} by A50, A65, A62, XBOOLE_0:def 4;

            then

             A66: (f1 /. ( len f1)) = (f1 /. k) by A3, TARSKI:def 1;

            k <= ( len f1) by A55, NAT_1: 11;

            then

             A67: k in ( dom f1) by A64, FINSEQ_3: 25;

            ( len f1) in ( dom f1) by FINSEQ_5: 6;

            

            then (( len f1) - k) = (( len f1) - ( len f1)) by A67, A66, PARTFUN2: 10

            .= 0 ;

            hence contradiction;

          end;

            suppose i <> 2;

            then 2 < i by A48, XXREAL_0: 1;

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

            then (( len f1) - i) <= (( len f1) - (1 + 2)) by XREAL_1: 10;

            then (( len f1) - i) <= ((( len f1) - 1) - 2);

            then

             A68: ((( len f1) - i) + (1 + 1)) <= k by XREAL_1: 19;

            ((( len f1) - i) + (1 + 1)) = (((m + (q .. f1)) + 1) + 1) by A58;

            then ((m + (q .. f1)) + 1) < k by A68, NAT_1: 13;

            then ( LSeg (f1,k)) misses ( LSeg (f1,(m + (q .. f1)))) by TOPREAL1:def 7;

            then (( LSeg (f1,k)) /\ ( LSeg (f1,(m + (q .. f1))))) = {} ;

            hence not p2 in ( LSeg (f19,i)) by A50, A56, XBOOLE_0:def 4;

          end;

        end;

        ( LSeg (f19,i)) c= ( L~ f19) by TOPREAL3: 19;

        then

         A69: not p1 in ( LSeg (f19,i)) by A32;

        ( LSeg ((f29 /. ( len f29)),(f19 /. 1))) c= ( L~ f2) by A27, TOPREAL3: 19;

        then

         A70: (( LSeg ((f29 /. ( len f29)),(f19 /. 1))) /\ ( LSeg (f19,i))) c= {p1, p2} by A5, A51, XBOOLE_1: 27;

        now

          given x be object such that

           A71: x in (( LSeg ((f29 /. ( len f29)),(f19 /. 1))) /\ ( LSeg (f19,i)));

          x = p1 or x = p2 by A70, A71, TARSKI:def 2;

          hence contradiction by A69, A52, A71, XBOOLE_0:def 4;

        end;

        then (( LSeg (f19,i)) /\ ( LSeg ((f29 /. ( len f29)),(f19 /. 1)))) = {} by XBOOLE_0:def 1;

        hence ( LSeg (f19,i)) misses ( LSeg ((f29 /. ( len f29)),(f19 /. 1)));

      end;

       A72:

      now

        assume ( len f19) <> 1;

        then 1 < ( len f19) by A19, XXREAL_0: 1;

        then

         A73: (1 + 1) <= ( len f19) by NAT_1: 13;

        now

          let x be object;

          hereby

            reconsider m = (( len f19) - 2) as Element of NAT by A73, INT_1: 5;

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

            then not p1 in ( LSeg (f19,1)) by A32;

            then

             A74: not p1 in (( LSeg ((f29 /. ( len f29)),(f19 /. 1))) /\ ( LSeg (f19,1))) by XBOOLE_0:def 4;

            ((m + 1) + 1) = ( len (f1 :- q)) by FINSEQ_5:def 3;

            

            then ( LSeg (f19,1)) = ( LSeg ((f1 :- q),(m + 1))) by Th2

            .= ( LSeg (f1,(m + (q .. f1)))) by A8, Th10;

            then

             A75: ( LSeg (f19,1)) c= ( L~ f1) by TOPREAL3: 19;

            ( LSeg ((f29 /. ( len f29)),(f19 /. 1))) c= ( L~ f2) by A27, TOPREAL3: 19;

            then

             A76: (( LSeg ((f29 /. ( len f29)),(f19 /. 1))) /\ ( LSeg (f19,1))) c= {p1, p2} by A5, A75, XBOOLE_1: 27;

            assume x in (( LSeg ((f29 /. ( len f29)),(f19 /. 1))) /\ ( LSeg (f19,1)));

            hence x = (f19 /. 1) by A4, A26, A76, A74, TARSKI:def 2;

          end;

          assume

           A77: x = (f19 /. 1);

          then x in ( LSeg ((f19 /. 1),(f19 /. (1 + 1)))) by RLTOPSP1: 68;

          then

           A78: x in ( LSeg (f19,1)) by A73, TOPREAL1:def 3;

          x in ( LSeg ((f29 /. ( len f29)),(f19 /. 1))) by A77, RLTOPSP1: 68;

          hence x in (( LSeg ((f29 /. ( len f29)),(f19 /. 1))) /\ ( LSeg (f19,1))) by A78, XBOOLE_0:def 4;

        end;

        hence (( LSeg ((f29 /. ( len f29)),(f19 /. 1))) /\ ( LSeg (f19,1))) = {(f19 /. 1)} by TARSKI:def 1;

      end;

      

       A79: ( len f29) >= 1 by A21, A23, FINSEQ_1: 59;

      then

       A80: f29 is non empty;

      (f1 :- q) is unfolded by A8, Th27;

      then

       A81: f19 is unfolded by Th28;

       A82:

      now

        per cases ;

          suppose ( len f29) = 1 & ( len f19) = 1;

          then ( len g2) = (1 + 1) by FINSEQ_1: 22;

          hence g2 is unfolded by Th26;

        end;

          suppose that

           A83: ( len f29) <> 1 and

           A84: ( len f19) = 1;

          consider k be Nat such that

           A85: (k + 1) = ( len f29) by A79, NAT_1: 6;

          reconsider k as Element of NAT by ORDINAL1:def 12;

          

           A86: ( LSeg (f29,k)) = ( LSeg (f2,k)) by A85, Th3;

          ( len f29) > 1 by A22, A23, A83, XXREAL_0: 1;

          then

           A87: 1 <= k by A85, NAT_1: 13;

          

           A88: f19 = <*(f19 . 1)*> by A84, FINSEQ_5: 14

          .= <*(f19 /. 1)*> by PARTFUN1:def 6, A20;

          (k + (1 + 1)) <= ( len f2) by A22, A85;

          then (( LSeg (f29,k)) /\ ( LSeg ((f29 /. ( len f29)),(f19 /. 1)))) = {(f29 /. ( len f29))} by A22, A25, A27, A85, A87, A86, TOPREAL1:def 6;

          hence g2 is unfolded by A85, A88, Th30;

        end;

          suppose that

           A89: ( len f29) = 1 and

           A90: ( len f19) <> 1;

          

           S: ( len f29) in ( dom f29) by FINSEQ_3: 25, A89;

          f29 = <*(f29 . ( len f29))*> by A89, FINSEQ_5: 14

          .= <*(f29 /. ( len f29))*> by PARTFUN1:def 6, S;

          hence g2 is unfolded by A81, A72, A90, Th29;

        end;

          suppose that

           A91: ( len f29) <> 1 and

           A92: ( len f19) <> 1;

          consider k be Nat such that

           A93: (k + 1) = ( len f29) by A79, NAT_1: 6;

          reconsider k as Element of NAT by ORDINAL1:def 12;

          

           A94: (k + (1 + 1)) <= ( len f2) by A22, A93;

          

           A95: ( LSeg (f29,k)) = ( LSeg (f2,k)) by A93, Th3;

          ( len f29) > 1 by A22, A23, A91, XXREAL_0: 1;

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

          then (( LSeg (f29,k)) /\ ( LSeg ((f29 /. ( len f29)),(f19 /. 1)))) = {(f29 /. ( len f29))} by A22, A25, A27, A93, A94, A95, TOPREAL1:def 6;

          hence g2 is unfolded by A81, A72, A92, A93, Th31;

        end;

      end;

      ( len g1) >= 2 by TOPREAL1:def 8;

      then

       A96: ( rng g1) c= ( L~ g1) by Th18;

      set Z = (( rng f29) /\ ( rng f19));

      

       A97: 1 in ( dom f29) by A22, A23, FINSEQ_3: 25;

      

       A98: ( len f2) in ( dom f2) by FINSEQ_5: 6;

      then

       A99: (p2 .. f2) = ( len f2) by A4, FINSEQ_5: 41;

      now

        assume

         A100: p2 in ( rng f29);

        then (p2 .. f29) = (p2 .. f2) by FINSEQ_5: 40;

        hence contradiction by A22, A99, A100, FINSEQ_4: 21, XREAL_1: 44;

      end;

      then

       A101: not p2 in Z by XBOOLE_0:def 4;

      then

       A102: Z <> {p1, p2} by TARSKI:def 2;

      ( dom f2) = ( Seg ( len f2)) by FINSEQ_1:def 3;

      then

       A103: ( len f29) in ( dom f2) by A22, A14, A24, A18, FINSEQ_2: 8;

      now

        p2 in ( LSeg ((f2 /. ( len f29)),p2)) by RLTOPSP1: 68;

        then

         A104: p2 in ( LSeg (f2,( len f29))) by A4, A22, A23, A14, TOPREAL1:def 3;

        assume p2 in ( L~ f29);

        then

        consider i such that

         A105: 1 <= i and

         A106: (i + 1) <= ( len f29) and

         A107: p2 in ( LSeg (f29,i)) by Th13;

        ( LSeg (f29,i)) = ( LSeg (f2,i)) by A106, Th3;

        then

         A108: p2 in (( LSeg (f2,i)) /\ ( LSeg (f2,( len f29)))) by A107, A104, XBOOLE_0:def 4;

        then

         A109: ( LSeg (f2,i)) meets ( LSeg (f2,( len f29)));

        

         A110: ( len f2) <> ( len f29) by A21, FINSEQ_1: 59;

        per cases ;

          suppose

           A111: (i + 1) = ( len f29);

          then (i + (1 + 1)) = ( len f2) by A22;

          then (( LSeg (f2,i)) /\ ( LSeg (f2,( len f29)))) = {(f2 /. ( len f29))} by A105, A111, TOPREAL1:def 6;

          then p2 = (f2 /. ( len f29)) by A108, TARSKI:def 1;

          hence contradiction by A4, A98, A103, A110, PARTFUN2: 10;

        end;

          suppose (i + 1) <> ( len f29);

          then (i + 1) < ( len f29) by A106, XXREAL_0: 1;

          hence contradiction by A109, TOPREAL1:def 7;

        end;

      end;

      then

       A112: not p2 in (( L~ f29) /\ ( L~ f19)) by XBOOLE_0:def 4;

      ( L~ (f1 :- q)) c= ( L~ f1) by A8, Lm15;

      then

       A113: ( L~ f19) c= ( L~ f1) by Th22;

      ( L~ f29) c= ( L~ f2) by Lm1;

      then (( L~ f29) /\ ( L~ f19)) c= {p1, p2} by A5, A113, XBOOLE_1: 27;

      then

       A114: (( L~ f29) /\ ( L~ f19)) = {} or (( L~ f29) /\ ( L~ f19)) = {p1} or (( L~ f29) /\ ( L~ f19)) = {p2} or (( L~ f29) /\ ( L~ f19)) = {p1, p2} by ZFMISC_1: 36;

      (f1 :- q) is special by A8, Th39;

      then

       A115: f19 is special by Th40;

      

       A116: 1 in ( dom (f1 :- q)) by FINSEQ_5: 6;

      now

        set l = (p1 .. (f1 :- q));

        assume

         A117: p1 in ( rng (f1 :- q));

        then

         A118: ((f1 :- q) . l) = p1 by FINSEQ_4: 19;

        l <> 0 by A117, FINSEQ_4: 21;

        then

        consider j be Nat such that

         A119: l = (j + 1) by NAT_1: 6;

        reconsider j as Element of NAT by ORDINAL1:def 12;

        

         A120: l in ( dom (f1 :- q)) by A117, FINSEQ_4: 20;

        then

         A121: (j + (q .. f1)) in ( dom f1) by A8, A119, FINSEQ_5: 51;

        ((f1 :- q) /. l) = (f1 /. (j + (q .. f1))) by A8, A120, A119, FINSEQ_5: 52;

        then (j + (q .. f1)) = 1 by A1, A31, A120, A118, A121, PARTFUN1:def 6, PARTFUN2: 10;

        then

         A122: (q .. f1) <= 1 by NAT_1: 11;

        1 <= (q .. f1) by A8, FINSEQ_4: 21;

        hence contradiction by A10, A122, XXREAL_0: 1;

      end;

      then not p1 in ( rng f19) by FINSEQ_5: 57;

      then not p1 in Z by XBOOLE_0:def 4;

      then

       A123: Z <> {p1} by TARSKI:def 1;

      ( rng f29) c= ( rng f2) by FINSEQ_5: 19;

      then Z c= (( rng f2) /\ ( rng f1)) by A15, XBOOLE_1: 27;

      then

       A124: Z c= {p1, p2} by A5, A17;

      reconsider f1q = (f1 :- q) as one-to-one FinSequence of ( TOP-REAL 2) by A8, FINSEQ_5: 56;

      

       A125: ( Rev f1q) is one-to-one;

      (f1 :- q) is s.n.c. by A8, Th34;

      then

       A126: f19 is s.n.c. by Th35;

      ((f29 /. ( len f29)) `1 ) = ((f19 /. 1) `1 ) or ((f29 /. ( len f29)) `2 ) = ((f19 /. 1) `2 ) by A23, A14, A25, A26, TOPREAL1:def 5;

      then

       A127: g2 is special by A115, Lm13;

      (( len f29) + ( len f19)) >= (1 + 1) by A22, A19, A23, XREAL_1: 7;

      then

       A128: ( len g2) >= 2 by FINSEQ_1: 22;

      Z <> {p2} by A101, TARSKI:def 1;

      then Z = {} by A123, A102, A124, ZFMISC_1: 36;

      then ( rng f29) misses ( rng f19);

      then

       A129: g2 is one-to-one by A125, FINSEQ_3: 91;

       not p1 in (( L~ f29) /\ ( L~ f19)) by A32, XBOOLE_0:def 4;

      then ( L~ f29) misses ( L~ f19) by A114, A112, TARSKI:def 1, TARSKI:def 2;

      then (f29 ^ f19) is s.n.c. by A126, A28, A47, Th36;

      then

      reconsider g2 as S-Sequence_in_R2 by A129, A128, A82, A127, TOPREAL1:def 8;

      

       A130: (( L~ f2) \/ ( L~ f19)) = (( L~ (f29 ^ <*p2*>)) \/ ( L~ f19)) by A4, A14, FINSEQ_5: 21

      .= ((( L~ f29) \/ ( LSeg ((f29 /. ( len f29)),(f19 /. 1)))) \/ ( L~ f19)) by A4, A97, A26, Th19, RELAT_1: 38

      .= ( L~ g2) by A20, A80, Th23, RELAT_1: 38;

      take g1, g2;

      thus

       A131: p1 = (g1 /. 1) by A1, A8, FINSEQ_5: 44;

      

       A132: 1 in ( dom g2) by FINSEQ_5: 6;

      

      hence

       A133: (g2 /. 1) = (g2 . 1) by PARTFUN1:def 6

      .= (f29 . 1) by A97, FINSEQ_1:def 7

      .= (f29 /. 1) by A97, PARTFUN1:def 6

      .= p1 by A2, A97, FINSEQ_4: 70;

      

      thus

       A134: q = (g1 /. (q .. f1)) by A8, FINSEQ_5: 45

      .= (g1 /. ( len g1)) by A8, FINSEQ_5: 42;

      

       A135: ( len g2) in ( dom g2) by FINSEQ_5: 6;

      

      hence

       A136: (g2 /. ( len g2)) = (g2 . ( len g2)) by PARTFUN1:def 6

      .= (g2 . (( len f29) + ( len f19))) by FINSEQ_1: 22

      .= (f19 . ( len f19)) by A20, FINSEQ_1:def 7

      .= (f19 . ( len (f1 :- q))) by FINSEQ_5:def 3

      .= ((f1 :- q) . 1) by FINSEQ_5: 62

      .= ((f1 :- q) /. 1) by A116, PARTFUN1:def 6

      .= q by FINSEQ_5: 53;

      ( len g2) >= 2 by TOPREAL1:def 8;

      then

       A137: ( rng g2) c= ( L~ g2) by Th18;

      

       A138: ( len g1) in ( dom g1) by FINSEQ_5: 6;

      thus {p1, q} = (( L~ g1) /\ ( L~ g2))

      proof

        hereby

          let x be object;

          assume

           A139: x in {p1, q};

          per cases by A139, TARSKI:def 2;

            suppose

             A140: x = p1;

            

             A141: p1 in ( rng g2) by A132, A133, PARTFUN2: 2;

            p1 in ( rng g1) by A131, A13, PARTFUN2: 2;

            hence x in (( L~ g1) /\ ( L~ g2)) by A96, A137, A140, A141, XBOOLE_0:def 4;

          end;

            suppose

             A142: x = q;

            

             A143: q in ( rng g2) by A135, A136, PARTFUN2: 2;

            q in ( rng g1) by A134, A138, PARTFUN2: 2;

            hence x in (( L~ g1) /\ ( L~ g2)) by A96, A137, A142, A143, XBOOLE_0:def 4;

          end;

        end;

        

         A144: ( len f1) in ( dom f1) by FINSEQ_5: 6;

        

         A145: (( L~ g1) /\ ( L~ g2)) = ((( L~ g1) /\ ( L~ f2)) \/ (( L~ g1) /\ ( L~ f19))) by A130, XBOOLE_1: 23;

        

         A146: (q .. f1) in ( dom f1) by A8, FINSEQ_4: 20;

        

         A147: q = (f1 . (q .. f1)) by A8, FINSEQ_4: 19

        .= (f1 /. (q .. f1)) by A146, PARTFUN1:def 6;

        

         A148: ( len g1) = (q .. f1) by A8, FINSEQ_5: 42;

        per cases ;

          suppose

           A149: q <> p2;

          now

            

             A150: (q .. f1) <= ( len f1) by A8, FINSEQ_4: 21;

            then

            reconsider j = (( len f1) - 1) as Element of NAT by A9, INT_1: 5, XXREAL_0: 2;

            

             A151: (j + 1) = ( len f1);

            

             A152: p2 in ( LSeg ((f1 /. j),(f1 /. (j + 1)))) by A3, RLTOPSP1: 68;

            1 < (q .. f1) by A10, A9, XXREAL_0: 1;

            then 1 < ( len f1) by A150, XXREAL_0: 2;

            then 1 <= j by A151, NAT_1: 13;

            then

             A153: p2 in ( LSeg (f1,j)) by A152, TOPREAL1:def 3;

            assume p2 in ( L~ g1);

            then

            consider i such that

             A154: 1 <= i and

             A155: (i + 1) <= ( len g1) and

             A156: p2 in ( LSeg (g1,i)) by Th13;

            

             A157: p2 in ( LSeg (f1,i)) by A155, A156, Th9;

            (q .. f1) < ( len f1) by A3, A147, A149, A150, XXREAL_0: 1;

            then

             A158: (q .. f1) <= j by A151, NAT_1: 13;

            then

             A159: (i + 1) <= j by A148, A155, XXREAL_0: 2;

            per cases ;

              suppose

               A160: (i + 1) = j;

              then (i + (1 + 1)) = (j + 1);

              then (( LSeg (f1,i)) /\ ( LSeg (f1,(i + 1)))) = {(f1 /. (i + 1))} by A154, TOPREAL1:def 6;

              then p2 in {(f1 /. (i + 1))} by A157, A153, A160, XBOOLE_0:def 4;

              then p2 = (f1 /. (i + 1)) by TARSKI:def 1;

              hence contradiction by A148, A147, A149, A155, A158, A160, XXREAL_0: 1;

            end;

              suppose (i + 1) <> j;

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

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

              then (( LSeg (f1,i)) /\ ( LSeg (f1,j))) = {} ;

              hence contradiction by A157, A153, XBOOLE_0:def 4;

            end;

          end;

          then

           A161: not p2 in (( L~ g1) /\ ( L~ f2)) by XBOOLE_0:def 4;

          (( L~ g1) /\ ( L~ f2)) c= {p1, p2} by A5, A8, Lm14, XBOOLE_1: 26;

          then (( L~ g1) /\ ( L~ f2)) = {} or (( L~ g1) /\ ( L~ f2)) = {p1} or (( L~ g1) /\ ( L~ f2)) = {p2} or (( L~ g1) /\ ( L~ f2)) = {p1, p2} by ZFMISC_1: 36;

          then

           A162: (( L~ g1) /\ ( L~ f2)) c= {p1} by A161, TARSKI:def 1, TARSKI:def 2;

          (( L~ g1) /\ ( L~ f19)) = (( L~ g1) /\ ( L~ (f1 :- q))) by Th22

          .= {q} by A3, A8, A10, A147, A149, Th42;

          then (( L~ g1) /\ ( L~ g2)) c= ( {p1} \/ {q}) by A145, A162, XBOOLE_1: 9;

          hence thesis by ENUMSET1: 1;

        end;

          suppose

           A163: q = p2;

          (p2 .. f1) = ( len f1) by A3, A144, FINSEQ_5: 41;

          

          then

           A164: ( len (f1 :- q)) = ((( len f1) - ( len f1)) + 1) by A8, A163, FINSEQ_5: 50

          .= ( 0 + 1);

          (( L~ g1) /\ ( L~ f19)) = (( L~ g1) /\ ( L~ (f1 :- q))) by Th22

          .= (( L~ g1) /\ {} ) by A164, TOPREAL1: 22

          .= {} ;

          hence thesis by A5, A8, A145, A163, Lm14, XBOOLE_1: 26;

        end;

      end;

      

      thus P = ((( L~ (f1 -: q)) \/ ( L~ (f1 :- q))) \/ ( L~ f2)) by A6, A8, Th24

      .= (( L~ g1) \/ (( L~ f2) \/ ( L~ (f1 :- q)))) by XBOOLE_1: 4

      .= (( L~ g1) \/ ( L~ g2)) by A130, Th22;

    end;

    theorem :: SPPOL_2:51

    

     Th51: (p1,p2) split P & q in P & q <> p1 implies (p1,q) split P

    proof

      assume p1 <> p2;

      given f1,f2 be S-Sequence_in_R2 such that

       A1: p1 = (f1 /. 1) and

       A2: p1 = (f2 /. 1) and

       A3: p2 = (f1 /. ( len f1)) and

       A4: p2 = (f2 /. ( len f2)) and

       A5: (( L~ f1) /\ ( L~ f2)) = {p1, p2} and

       A6: P = (( L~ f1) \/ ( L~ f2));

      assume

       A7: q in P;

      assume

       A8: q <> p1;

      hence p1 <> q;

      per cases by A6, A7, XBOOLE_0:def 3;

        suppose

         A9: q in ( L~ f1);

        now

          per cases ;

            suppose q in ( rng f1);

            hence thesis by A1, A2, A3, A4, A5, A6, A8, Lm16;

          end;

            suppose

             A10: not q in ( rng f1);

            consider i such that

             A11: 1 <= i and

             A12: (i + 1) <= ( len f1) and

             A13: q in ( LSeg (f1,i)) by A9, Th13;

            reconsider f19 = ( Ins (f1,i,q)) as S-Sequence_in_R2 by A10, A13, Th48;

            

             A14: ( L~ f19) = ( L~ f1) by A13, Th25;

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

            then 1 <= ( len f1) by A12, XXREAL_0: 2;

            then

             Z: 1 in ( dom f1) & ( len f1) in ( dom f1) by FINSEQ_3: 25;

            then

             a3: p2 = (f1 . ( len f1)) by A3, PARTFUN1:def 6;

            

             S2: ( len f19) = (( len f1) + 1) by FINSEQ_5: 69;

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

            then 1 <= ( len f19) by S2;

            then

             S1: ( len f19) in ( dom f19) & 1 in ( dom f19) by FINSEQ_3: 25;

            

             A15: p2 = (f19 . ( len f19)) by A12, a3, FINSEQ_5: 74, S2

            .= (f19 /. ( len f19)) by S1, PARTFUN1:def 6;

            

             A16: q in ( rng f19) by FINSEQ_5: 71;

            p1 = (f1 . 1) by Z, A1, PARTFUN1:def 6;

            

            then p1 = (f19 . 1) by A11, FINSEQ_5: 75

            .= (f19 /. 1) by PARTFUN1:def 6, S1;

            hence thesis by A2, A4, A5, A6, A8, A16, A15, A14, Lm16;

          end;

        end;

        hence thesis;

      end;

        suppose

         A17: q in ( L~ f2);

        now

          per cases ;

            suppose q in ( rng f2);

            hence thesis by A1, A2, A3, A4, A5, A6, A8, Lm16;

          end;

            suppose

             A18: not q in ( rng f2);

            consider i such that

             A19: 1 <= i and

             A20: (i + 1) <= ( len f2) and

             A21: q in ( LSeg (f2,i)) by A17, Th13;

            reconsider f29 = ( Ins (f2,i,q)) as S-Sequence_in_R2 by A18, A21, Th48;

            

             A22: ( L~ f29) = ( L~ f2) by A21, Th25;

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

            then 1 <= ( len f2) by A20, XXREAL_0: 2;

            then

             Z: 1 in ( dom f2) & ( len f2) in ( dom f2) by FINSEQ_3: 25;

            then

             Sa: p2 = (f2 . ( len f2)) by PARTFUN1:def 6, A4;

            

             Sc: ( len f29) = (( len f2) + 1) by FINSEQ_5: 69;

            then 1 <= ( len f29) by NAT_1: 11;

            then

             Sd: 1 in ( dom f29) & ( len f29) in ( dom f29) by FINSEQ_3: 25;

            

             A23: p2 = (f29 . ( len f29)) by Sc, Sa, A20, FINSEQ_5: 74

            .= (f29 /. ( len f29)) by PARTFUN1:def 6, Sd;

            

             A24: q in ( rng f29) by FINSEQ_5: 71;

            p1 = (f2 . 1) by PARTFUN1:def 6, A2, Z;

            

            then p1 = (f29 . 1) by A19, FINSEQ_5: 75

            .= (f29 /. 1) by Sd, PARTFUN1:def 6;

            hence thesis by A1, A3, A5, A6, A8, A24, A23, A22, Lm16;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: SPPOL_2:52

    

     Th52: (p1,p2) split P & q in P & q <> p2 implies (q,p2) split P

    proof

      assume that

       A1: (p1,p2) split P and

       A2: q in P and

       A3: q <> p2;

      (p2,p1) split P by A1, Th50;

      then (p2,q) split P by A2, A3, Th51;

      hence thesis by Th50;

    end;

    theorem :: SPPOL_2:53

    

     Th53: (p1,p2) split P & q1 in P & q2 in P & q1 <> q2 implies (q1,q2) split P

    proof

      assume that

       A1: (p1,p2) split P and

       A2: q1 in P and

       A3: q2 in P and

       A4: q1 <> q2;

      

       A5: (p2,p1) split P by A1, Th50;

      per cases ;

        suppose p1 = q1;

        hence thesis by A1, A3, A4, Th51;

      end;

        suppose p1 = q2;

        hence thesis by A2, A4, A5, Th52;

      end;

        suppose p1 <> q1;

        then (p1,q1) split P by A1, A2, Th51;

        then (q2,q1) split P by A3, A4, Th52;

        hence thesis by Th50;

      end;

        suppose p2 <> q1;

        then (q1,p2) split P by A1, A2, Th52;

        hence thesis by A3, A4, Th51;

      end;

    end;

    notation

      let P be Subset of ( TOP-REAL 2);

      synonym P is special_polygonal for P is being_special_polygon;

    end

    definition

      let P be Subset of ( TOP-REAL 2);

      :: original: special_polygonal

      redefine

      :: SPPOL_2:def2

      attr P is special_polygonal means ex p1, p2 st (p1,p2) split P;

      compatibility

      proof

        thus P is being_special_polygon implies ex p1, p2 st (p1,p2) split P

        proof

          given p1,p2 be Point of ( TOP-REAL 2), P1,P2 be Subset of ( TOP-REAL 2) such that

           A1: p1 <> p2 and p1 in P and p2 in P and

           A2: P1 is_S-P_arc_joining (p1,p2) and

           A3: P2 is_S-P_arc_joining (p1,p2) and

           A4: (P1 /\ P2) = {p1, p2} and

           A5: P = (P1 \/ P2);

          take p1, p2;

          thus p1 <> p2 by A1;

          consider f1 such that

           A6: f1 is being_S-Seq and

           A7: P1 = ( L~ f1) and

           A8: p1 = (f1 /. 1) and

           A9: p2 = (f1 /. ( len f1)) by A2;

          consider f2 such that

           A10: f2 is being_S-Seq and

           A11: P2 = ( L~ f2) and

           A12: p1 = (f2 /. 1) and

           A13: p2 = (f2 /. ( len f2)) by A3;

          reconsider f1, f2 as S-Sequence_in_R2 by A6, A10;

          take f1, f2;

          thus thesis by A4, A5, A7, A8, A9, A11, A12, A13;

        end;

        given p1, p2 such that

         A14: (p1,p2) split P;

        

         A15: p2 in {p1, p2} by TARSKI:def 2;

        

         A16: p1 in {p1, p2} by TARSKI:def 2;

        consider f1,f2 be S-Sequence_in_R2 such that

         A17: p1 = (f1 /. 1) and

         A18: p1 = (f2 /. 1) and

         A19: p2 = (f1 /. ( len f1)) and

         A20: p2 = (f2 /. ( len f2)) and

         A21: (( L~ f1) /\ ( L~ f2)) = {p1, p2} and

         A22: P = (( L~ f1) \/ ( L~ f2)) by A14;

        take p1, p2, P1 = ( L~ f1), P2 = ( L~ f2);

        thus p1 <> p2 by A14;

         {p1, p2} c= P by A21, A22, XBOOLE_1: 29;

        hence p1 in P & p2 in P by A16, A15;

        thus ex f st f is being_S-Seq & P1 = ( L~ f) & p1 = (f /. 1) & p2 = (f /. ( len f)) by A17, A19;

        thus ex f st f is being_S-Seq & P2 = ( L~ f) & p1 = (f /. 1) & p2 = (f /. ( len f)) by A18, A20;

        thus thesis by A21, A22;

      end;

    end

    definition

      let r1,r2,r19,r29 be Real;

      :: SPPOL_2:def3

      func [.r1,r2,r19,r29.] -> Subset of ( TOP-REAL 2) equals ((( LSeg ( |[r1, r19]|, |[r1, r29]|)) \/ ( LSeg ( |[r1, r29]|, |[r2, r29]|))) \/ (( LSeg ( |[r2, r29]|, |[r2, r19]|)) \/ ( LSeg ( |[r2, r19]|, |[r1, r19]|))));

      coherence ;

    end

    registration

      let n be Element of NAT ;

      let p1,p2 be Point of ( TOP-REAL n);

      cluster ( LSeg (p1,p2)) -> compact;

      coherence ;

    end

    registration

      let r1, r2, r19, r29;

      cluster [.r1, r2, r19, r29.] -> non empty compact;

      coherence

      proof

        thus [.r1, r2, r19, r29.] is non empty;

        

         A1: (( LSeg ( |[r2, r29]|, |[r2, r19]|)) \/ ( LSeg ( |[r2, r19]|, |[r1, r19]|))) is compact by COMPTS_1: 10;

        (( LSeg ( |[r1, r19]|, |[r1, r29]|)) \/ ( LSeg ( |[r1, r29]|, |[r2, r29]|))) is compact by COMPTS_1: 10;

        hence thesis by A1, COMPTS_1: 10;

      end;

    end

    theorem :: SPPOL_2:54

    r1 <= r2 & r19 <= r29 implies [.r1, r2, r19, r29.] = { p : (p `1 ) = r1 & (p `2 ) <= r29 & (p `2 ) >= r19 or (p `1 ) <= r2 & (p `1 ) >= r1 & (p `2 ) = r29 or (p `1 ) <= r2 & (p `1 ) >= r1 & (p `2 ) = r19 or (p `1 ) = r2 & (p `2 ) <= r29 & (p `2 ) >= r19 }

    proof

      assume that

       A1: r1 <= r2 and

       A2: r19 <= r29;

      set p1 = |[r1, r19]|, p2 = |[r1, r29]|, p3 = |[r2, r29]|, p4 = |[r2, r19]|;

      set P4 = { p : (p `2 ) = r19 & r1 <= (p `1 ) & (p `1 ) <= r2 };

      set P3 = { p : (p `1 ) = r2 & r19 <= (p `2 ) & (p `2 ) <= r29 };

      set P2 = { p : (p `2 ) = r29 & r1 <= (p `1 ) & (p `1 ) <= r2 };

      set P1 = { p : (p `1 ) = r1 & r19 <= (p `2 ) & (p `2 ) <= r29 };

      set P = { p : (p `1 ) = r1 & (p `2 ) <= r29 & (p `2 ) >= r19 or (p `1 ) <= r2 & (p `1 ) >= r1 & (p `2 ) = r29 or (p `1 ) <= r2 & (p `1 ) >= r1 & (p `2 ) = r19 or (p `1 ) = r2 & (p `2 ) <= r29 & (p `2 ) >= r19 };

      

       A3: P = ((P1 \/ P2) \/ (P3 \/ P4))

      proof

        hereby

          let x be object;

          assume x in P;

          then ex p st x = p & ((p `1 ) = r1 & (p `2 ) <= r29 & (p `2 ) >= r19 or (p `1 ) <= r2 & (p `1 ) >= r1 & (p `2 ) = r29 or (p `1 ) <= r2 & (p `1 ) >= r1 & (p `2 ) = r19 or (p `1 ) = r2 & (p `2 ) <= r29 & (p `2 ) >= r19);

          then x in P1 or x in P2 or x in P3 or x in P4;

          then x in (P1 \/ P2) or x in (P3 \/ P4) by XBOOLE_0:def 3;

          hence x in ((P1 \/ P2) \/ (P3 \/ P4)) by XBOOLE_0:def 3;

        end;

        let x be object;

        assume x in ((P1 \/ P2) \/ (P3 \/ P4));

        then

         A4: x in (P1 \/ P2) or x in (P3 \/ P4) by XBOOLE_0:def 3;

        per cases by A4, XBOOLE_0:def 3;

          suppose x in P1;

          then ex p st x = p & (p `1 ) = r1 & r19 <= (p `2 ) & (p `2 ) <= r29;

          hence thesis;

        end;

          suppose x in P2;

          then ex p st x = p & (p `2 ) = r29 & r1 <= (p `1 ) & (p `1 ) <= r2;

          hence thesis;

        end;

          suppose x in P3;

          then ex p st x = p & (p `1 ) = r2 & r19 <= (p `2 ) & (p `2 ) <= r29;

          hence thesis;

        end;

          suppose x in P4;

          then ex p st x = p & (p `2 ) = r19 & r1 <= (p `1 ) & (p `1 ) <= r2;

          hence thesis;

        end;

      end;

      

      thus [.r1, r2, r19, r29.] = ((P1 \/ ( LSeg (p2,p3))) \/ (( LSeg (p3,p4)) \/ ( LSeg (p4,p1)))) by A2, TOPREAL3: 9

      .= ((P1 \/ P2) \/ (( LSeg (p3,p4)) \/ ( LSeg (p4,p1)))) by A1, TOPREAL3: 10

      .= ((P1 \/ P2) \/ (P3 \/ ( LSeg (p4,p1)))) by A2, TOPREAL3: 9

      .= P by A1, A3, TOPREAL3: 10;

    end;

    theorem :: SPPOL_2:55

    

     Th55: r1 <> r2 & r19 <> r29 implies [.r1, r2, r19, r29.] is special_polygonal

    proof

      assume that

       A1: r1 <> r2 and

       A2: r19 <> r29;

      set p1 = |[r1, r19]|, p2 = |[r1, r29]|, p3 = |[r2, r29]|, p4 = |[r2, r19]|;

      

       A3: (p3 `1 ) = r2 by EUCLID: 52;

      take p1, p3;

      thus p1 <> p3 by A1, FINSEQ_1: 77;

      

       A4: (p4 `1 ) = r2 by EUCLID: 52;

      

       A5: (p3 `2 ) = r29 by EUCLID: 52;

      

       A6: (p4 `2 ) = r19 by EUCLID: 52;

      set f1 = <*p1, p2, p3*>, f2 = <*p1, p4, p3*>;

      

       A7: (p1 `1 ) = r1 by EUCLID: 52;

      

       A8: ( len f2) = 3 by FINSEQ_1: 45;

      

       A9: ( len f1) = 3 by FINSEQ_1: 45;

      

       A10: (p1 `2 ) = r19 by EUCLID: 52;

      then

      reconsider f1, f2 as S-Sequence_in_R2 by A1, A2, A7, A3, A5, TOPREAL3: 34, TOPREAL3: 35;

      take f1, f2;

      thus p1 = (f1 /. 1) & p1 = (f2 /. 1) & p3 = (f1 /. ( len f1)) & p3 = (f2 /. ( len f2)) by A9, A8, FINSEQ_4: 18;

      

       A11: ( L~ f2) = (( LSeg (p3,p4)) \/ ( LSeg (p4,p1))) by TOPREAL3: 16;

      ( L~ f1) = (( LSeg (p1,p2)) \/ ( LSeg (p2,p3))) by TOPREAL3: 16;

      

      hence (( L~ f1) /\ ( L~ f2)) = (((( LSeg (p1,p2)) \/ ( LSeg (p2,p3))) /\ ( LSeg (p3,p4))) \/ ((( LSeg (p1,p2)) \/ ( LSeg (p2,p3))) /\ ( LSeg (p4,p1)))) by A11, XBOOLE_1: 23

      .= (((( LSeg (p2,p1)) \/ ( LSeg (p3,p2))) /\ ( LSeg (p4,p3))) \/ {p1}) by A2, A7, A10, A5, A6, TOPREAL3: 27

      .= ( {p3} \/ {p1}) by A1, A7, A3, A5, A4, TOPREAL3: 28

      .= {p1, p3} by ENUMSET1: 1;

      thus thesis by A11, TOPREAL3: 16;

    end;

    theorem :: SPPOL_2:56

    

     Th56: R^2-unit_square = [. 0 , 1, 0 , 1.];

    registration

      cluster special_polygonal for Subset of ( TOP-REAL 2);

      existence

      proof

        take [. 0 , 1, 0 , 1.];

        thus thesis by Th55;

      end;

    end

    registration

      cluster R^2-unit_square -> special_polygonal;

      coherence by Th55, Th56;

    end

    registration

      cluster special_polygonal for Subset of ( TOP-REAL 2);

      existence by Th56;

      cluster special_polygonal -> non empty for Subset of ( TOP-REAL 2);

      coherence ;

      cluster special_polygonal -> non trivial for Subset of ( TOP-REAL 2);

      coherence by ZFMISC_1:def 10;

    end

    definition

      mode Special_polygon_in_R2 is special_polygonal Subset of ( TOP-REAL 2);

    end

    theorem :: SPPOL_2:57

    

     Th57: P is being_S-P_arc implies P is compact

    proof

      

       A1: I[01] is compact by HEINE: 4, TOPMETR: 20;

      assume P is being_S-P_arc;

      then

      reconsider P as being_S-P_arc Subset of ( TOP-REAL 2);

      consider f be Function of I[01] , (( TOP-REAL 2) | P) such that

       A2: f is being_homeomorphism by TOPREAL1: 29;

      

       A3: ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A2, TOPS_2:def 5;

      f is continuous by A2, TOPS_2:def 5;

      then (( TOP-REAL 2) | P) is compact by A1, A3, COMPTS_1: 14;

      hence thesis by COMPTS_1: 3;

    end;

    registration

      cluster -> compact for Special_polygon_in_R2;

      coherence

      proof

        let G be Special_polygon_in_R2;

        consider p,q be Point of ( TOP-REAL 2), P1,P2 be Subset of ( TOP-REAL 2) such that p <> q and p in G and q in G and

         A1: P1 is_S-P_arc_joining (p,q) and

         A2: P2 is_S-P_arc_joining (p,q) and (P1 /\ P2) = {p, q} and

         A3: G = (P1 \/ P2) by TOPREAL4:def 2;

        reconsider P1, P2 as Subset of ( TOP-REAL 2);

        

         A4: P2 is compact by A2, Th57, TOPREAL4: 1;

        P1 is compact by A1, Th57, TOPREAL4: 1;

        hence thesis by A3, A4, COMPTS_1: 10;

      end;

    end

    theorem :: SPPOL_2:58

    

     Th58: P is special_polygonal implies for p1, p2 st p1 <> p2 & p1 in P & p2 in P holds (p1,p2) split P by Th53;

    theorem :: SPPOL_2:59

    P is special_polygonal implies for p1, p2 st p1 <> p2 & p1 in P & p2 in P holds ex P1,P2 be Subset of ( TOP-REAL 2) st P1 is_S-P_arc_joining (p1,p2) & P2 is_S-P_arc_joining (p1,p2) & (P1 /\ P2) = {p1, p2} & P = (P1 \/ P2)

    proof

      assume

       A1: P is special_polygonal;

      let p1, p2;

      assume that

       A2: p1 <> p2 and

       A3: p1 in P and

       A4: p2 in P;

      (p1,p2) split P by A1, A2, A3, A4, Th58;

      then

      consider f1,f2 be S-Sequence_in_R2 such that

       A5: p1 = (f1 /. 1) and

       A6: p1 = (f2 /. 1) and

       A7: p2 = (f1 /. ( len f1)) and

       A8: p2 = (f2 /. ( len f2)) and

       A9: (( L~ f1) /\ ( L~ f2)) = {p1, p2} and

       A10: P = (( L~ f1) \/ ( L~ f2));

      take P1 = ( L~ f1), P2 = ( L~ f2);

      thus P1 is_S-P_arc_joining (p1,p2) by A5, A7;

      thus P2 is_S-P_arc_joining (p1,p2) by A6, A8;

      thus thesis by A9, A10;

    end;