graph_4.miz



    begin

    reserve p,q for FinSequence,

e,X for set,

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

G for Graph;

    reserve x,y,v,v1,v2,v3,v4 for Element of G;

    definition

      let G;

      let x, y;

      let e;

      :: GRAPH_4:def1

      pred e orientedly_joins x,y means (the Source of G . e) = x & (the Target of G . e) = y;

    end

    theorem :: GRAPH_4:1

    

     Th1: e orientedly_joins (v1,v2) implies e joins (v1,v2) by GRAPH_1:def 12;

    definition

      let G;

      let x,y be Element of the carrier of G;

      :: GRAPH_4:def2

      pred x,y are_orientedly_incident means ex v be set st v in the carrier' of G & v orientedly_joins (x,y);

    end

    theorem :: GRAPH_4:2

    e orientedly_joins (v1,v2) & e orientedly_joins (v3,v4) implies v1 = v3 & v2 = v4;

    reserve vs,vs1,vs2 for FinSequence of the carrier of G,

c,c1,c2 for oriented Chain of G;

    definition

      let G, X;

      :: GRAPH_4:def3

      func G -SVSet X -> set equals { v : ex e be Element of the carrier' of G st e in X & v = (the Source of G . e) };

      correctness ;

    end

    definition

      let G, X;

      :: GRAPH_4:def4

      func G -TVSet X -> set equals { v : ex e be Element of the carrier' of G st e in X & v = (the Target of G . e) };

      correctness ;

    end

    theorem :: GRAPH_4:3

    (G -SVSet {} ) = {} & (G -TVSet {} ) = {}

    proof

      set X = {} ;

       A1:

      now

        assume

         A2: (G -SVSet X) <> {} ;

        set x = the Element of (G -SVSet X);

        x in (G -SVSet X) by A2;

        then ex v st (v = x) & (ex e be Element of the carrier' of G st e in X & v = (the Source of G . e));

        hence contradiction;

      end;

      now

        assume

         A3: (G -TVSet X) <> {} ;

        set x = the Element of (G -TVSet X);

        x in (G -TVSet X) by A3;

        then ex v st (v = x) & (ex e be Element of the carrier' of G st e in X & v = (the Target of G . e));

        hence contradiction;

      end;

      hence thesis by A1;

    end;

    definition

      let G, vs;

      let c be FinSequence;

      :: GRAPH_4:def5

      pred vs is_oriented_vertex_seq_of c means ( len vs) = (( len c) + 1) & for n st 1 <= n & n <= ( len c) holds (c . n) orientedly_joins ((vs /. n),(vs /. (n + 1)));

    end

    theorem :: GRAPH_4:4

    

     Th4: vs is_oriented_vertex_seq_of c implies vs is_vertex_seq_of c

    proof

      assume

       A1: vs is_oriented_vertex_seq_of c;

      then

       A2: ( len vs) = (( len c) + 1);

      for n st 1 <= n & n <= ( len c) holds (c . n) joins ((vs /. n),(vs /. (n + 1))) by A1, Th1;

      hence thesis by A2, GRAPH_2:def 6;

    end;

    theorem :: GRAPH_4:5

    vs is_oriented_vertex_seq_of c implies (G -SVSet ( rng c)) c= ( rng vs)

    proof

      assume

       A1: vs is_oriented_vertex_seq_of c;

      then

       A2: ( len vs) = (( len c) + 1);

      (G -SVSet ( rng c)) c= ( rng vs)

      proof

        let y be object;

        assume y in (G -SVSet ( rng c));

        then

        consider v be Element of G such that

         A3: v = y and

         A4: ex e be Element of the carrier' of G st e in ( rng c) & v = (the Source of G . e);

        consider e be Element of the carrier' of G such that

         A5: e in ( rng c) and

         A6: v = (the Source of G . e) by A4;

        consider x be object such that

         A7: x in ( dom c) and

         A8: e = (c . x) by A5, FUNCT_1:def 3;

        reconsider x as Element of NAT by A7;

        

         A9: 1 <= x by A7, FINSEQ_3: 25;

        

         A10: x <= ( len c) by A7, FINSEQ_3: 25;

        then

         A11: x <= ( len vs) by A2, NAT_1: 12;

        set v1 = (vs /. x);

        set v2 = (vs /. (x + 1));

        

         A12: v1 = (vs . x) by A9, A11, FINSEQ_4: 15;

        (c . x) orientedly_joins (v1,v2) by A1, A9, A10;

        then

         A13: v = v1 by A6, A8;

        x in ( dom vs) by A9, A11, FINSEQ_3: 25;

        hence thesis by A3, A12, A13, FUNCT_1:def 3;

      end;

      hence thesis;

    end;

    theorem :: GRAPH_4:6

    vs is_oriented_vertex_seq_of c implies (G -TVSet ( rng c)) c= ( rng vs)

    proof

      assume

       A1: vs is_oriented_vertex_seq_of c;

      then

       A2: ( len vs) = (( len c) + 1);

      let y be object;

      assume y in (G -TVSet ( rng c));

      then

      consider v be Element of G such that

       A3: v = y and

       A4: ex e be Element of the carrier' of G st e in ( rng c) & v = (the Target of G . e);

      consider e be Element of the carrier' of G such that

       A5: e in ( rng c) and

       A6: v = (the Target of G . e) by A4;

      consider x be object such that

       A7: x in ( dom c) and

       A8: e = (c . x) by A5, FUNCT_1:def 3;

      reconsider x as Element of NAT by A7;

      

       A9: 1 <= x by A7, FINSEQ_3: 25;

      

       A10: x <= ( len c) by A7, FINSEQ_3: 25;

      

       A11: 1 <= (x + 1) by NAT_1: 12;

      

       A12: (x + 1) <= ( len vs) by A2, A10, XREAL_1: 7;

      set v1 = (vs /. x);

      set v2 = (vs /. (x + 1));

      

       A13: v2 = (vs . (x + 1)) by A2, A10, A11, FINSEQ_4: 15, XREAL_1: 7;

      (c . x) orientedly_joins (v1,v2) by A1, A9, A10;

      then

       A14: v = v2 by A6, A8;

      (x + 1) in ( dom vs) by A11, A12, FINSEQ_3: 25;

      hence thesis by A3, A13, A14, FUNCT_1:def 3;

    end;

    theorem :: GRAPH_4:7

    c <> {} & vs is_oriented_vertex_seq_of c implies ( rng vs) c= ((G -SVSet ( rng c)) \/ (G -TVSet ( rng c)))

    proof

      assume that

       A1: c <> {} and

       A2: vs is_oriented_vertex_seq_of c;

      

       A3: ( len vs) = (( len c) + 1) by A2;

      let y be object;

      assume y in ( rng vs);

      then

      consider x be object such that

       A4: x in ( dom vs) and

       A5: y = (vs . x) by FUNCT_1:def 3;

      reconsider x as Element of NAT by A4;

      

       A6: 1 <= x by A4, FINSEQ_3: 25;

      

       A7: x <= ( len vs) by A4, FINSEQ_3: 25;

      per cases by A3, A7, NAT_1: 8;

        suppose

         A8: x <= ( len c);

        then x in ( dom c) by A6, FINSEQ_3: 25;

        then

         A9: (c . x) in ( rng c) by FUNCT_1:def 3;

        ( rng c) c= the carrier' of G by FINSEQ_1:def 4;

        then

        reconsider e = (c . x) as Element of the carrier' of G by A9;

        set v1 = (vs /. x);

        set v2 = (vs /. (x + 1));

        

         A10: v1 = (vs . x) by A6, A7, FINSEQ_4: 15;

        (c . x) orientedly_joins (v1,v2) by A2, A6, A8;

        then

         A11: v1 = (the Source of G . e);

        x in ( dom c) by A6, A8, FINSEQ_3: 25;

        then e in ( rng c) by FUNCT_1:def 3;

        then y in (G -SVSet ( rng c)) by A5, A10, A11;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose

         A12: x = (( len c) + 1);

        set l = ( len c);

        ( 0 + 1) = 1;

        then

         A13: 1 <= l by A1, NAT_1: 13;

        then l in ( dom c) by FINSEQ_3: 25;

        then

         A14: (c . l) in ( rng c) by FUNCT_1:def 3;

        ( rng c) c= the carrier' of G by FINSEQ_1:def 4;

        then

        reconsider e = (c . l) as Element of the carrier' of G by A14;

        set v1 = (vs /. l);

        set v2 = (vs /. (l + 1));

        

         A15: v2 = (vs . (l + 1)) by A3, A6, A12, FINSEQ_4: 15;

        (c . l) orientedly_joins (v1,v2) by A2, A13;

        then

         A16: v2 = (the Target of G . e);

        l in ( dom c) by A13, FINSEQ_3: 25;

        then e in ( rng c) by FUNCT_1:def 3;

        then y in (G -TVSet ( rng c)) by A5, A12, A15, A16;

        hence thesis by XBOOLE_0:def 3;

      end;

    end;

    begin

    theorem :: GRAPH_4:8

     <*v*> is_oriented_vertex_seq_of {} by FINSEQ_1: 40;

    theorem :: GRAPH_4:9

    

     Th9: ex vs st vs is_oriented_vertex_seq_of c

    proof

      now

        per cases ;

          case

           A1: c <> {} ;

          defpred P[ Nat, object] means (($1 = (( len c) + 1) implies $2 = (the Target of G . (c . ( len c)))) & ($1 <> (( len c) + 1) implies $2 = (the Source of G . (c . $1))));

          

           A2: for k be Nat st k in ( Seg (( len c) + 1)) holds ex x be object st P[k, x]

          proof

            let k be Nat;

            assume k in ( Seg (( len c) + 1));

            now

              per cases ;

                case k = (( len c) + 1);

                hence thesis;

              end;

                case k <> (( len c) + 1);

                hence thesis;

              end;

            end;

            hence thesis;

          end;

          ex p st ( dom p) = ( Seg (( len c) + 1)) & for k be Nat st k in ( Seg (( len c) + 1)) holds P[k, (p . k)] from FINSEQ_1:sch 1( A2);

          then

          consider p such that

           A3: ( dom p) = ( Seg (( len c) + 1)) and

           A4: for k be Nat st k in ( Seg (( len c) + 1)) holds (k = (( len c) + 1) implies (p . k) = (the Target of G . (c . ( len c)))) & (k <> (( len c) + 1) implies (p . k) = (the Source of G . (c . k)));

          

           A5: ( len p) = (( len c) + 1) by A3, FINSEQ_1:def 3;

          ( rng p) c= the carrier of G

          proof

            let y be object;

            assume y in ( rng p);

            then

            consider x be object such that

             A6: x in ( dom p) and

             A7: y = (p . x) by FUNCT_1:def 3;

            reconsider k = x as Element of NAT by A6;

            

             A8: 1 <= k by A3, A6, FINSEQ_1: 1;

            

             A9: k <= (( len c) + 1) by A3, A6, FINSEQ_1: 1;

            now

              per cases ;

                case k = (( len c) + 1);

                then

                 A10: y = (the Target of G . (c . ( len c))) by A3, A4, A6, A7;

                ( len c) >= ( 0 + 1) by A1, NAT_1: 13;

                then ( len c) in ( Seg ( len c)) by FINSEQ_1: 1;

                then ( len c) in ( dom c) by FINSEQ_1:def 3;

                then

                 A11: (c . ( len c)) in ( rng c) by FUNCT_1:def 3;

                ( rng c) c= the carrier' of G by FINSEQ_1:def 4;

                hence thesis by A10, A11, FUNCT_2: 5;

              end;

                case

                 A12: k <> (( len c) + 1);

                then

                 A13: y = (the Source of G . (c . k)) by A3, A4, A6, A7;

                k < (( len c) + 1) by A9, A12, XXREAL_0: 1;

                then k <= ( len c) by NAT_1: 13;

                then k in ( Seg ( len c)) by A8, FINSEQ_1: 1;

                then k in ( dom c) by FINSEQ_1:def 3;

                then

                 A14: (c . k) in ( rng c) by FUNCT_1:def 3;

                ( rng c) c= the carrier' of G by FINSEQ_1:def 4;

                hence thesis by A13, A14, FUNCT_2: 5;

              end;

            end;

            hence thesis;

          end;

          then

          reconsider vs = p as FinSequence of the carrier of G by FINSEQ_1:def 4;

          for n st 1 <= n & n <= ( len c) holds (c . n) orientedly_joins ((vs /. n),(vs /. (n + 1)))

          proof

            let n;

            assume that

             A15: 1 <= n and

             A16: n <= ( len c);

            per cases ;

              suppose

               A17: n = ( len c);

              then

               A18: n < (( len c) + 1) by NAT_1: 13;

              then n in ( Seg (( len c) + 1)) by A15, FINSEQ_1: 1;

              then

               A19: (p . n) = (the Source of G . (c . n)) by A4, A18;

              1 < (n + 1) by A15, NAT_1: 13;

              then (n + 1) in ( Seg (( len c) + 1)) by A17, FINSEQ_1: 1;

              then

               A20: (p . (n + 1)) = (the Target of G . (c . ( len c))) by A4, A17;

              

               A21: (the Source of G . (c . n)) = (vs /. n) by A5, A15, A18, A19, FINSEQ_4: 15;

              1 < (n + 1) by A15, NAT_1: 13;

              then (the Target of G . (c . n)) = (vs /. (n + 1)) by A5, A17, A20, FINSEQ_4: 15;

              hence thesis by A21;

            end;

              suppose n <> ( len c);

              then

               A22: n < ( len c) by A16, XXREAL_0: 1;

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

              then

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

              

               A24: n < (( len c) + 1) by A16, NAT_1: 13;

              then n in ( Seg (( len c) + 1)) by A15, FINSEQ_1: 1;

              then

               A25: (p . n) = (the Source of G . (c . n)) by A4, A24;

              1 < (n + 1) by A15, NAT_1: 13;

              then (n + 1) in ( Seg (( len c) + 1)) by A23, FINSEQ_1: 1;

              then

               A26: (p . (n + 1)) = (the Source of G . (c . (n + 1))) by A4, A23;

              

               A27: (the Source of G . (c . n)) = (vs /. n) by A5, A15, A24, A25, FINSEQ_4: 15;

              1 < (n + 1) by A15, NAT_1: 13;

              then (vs /. (n + 1)) = (p . (n + 1)) by A5, A23, FINSEQ_4: 15;

              then (the Target of G . (c . n)) = (vs /. (n + 1)) by A15, A22, A26, GRAPH_1:def 15;

              hence thesis by A27;

            end;

          end;

          then vs is_oriented_vertex_seq_of c by A5;

          hence thesis;

        end;

          case

           A28: c = {} ;

          set x = the Element of G;

          set vs = <*x*>;

          ( len c) = 0 by A28;

          then

           A29: ( len vs) = (( len c) + 1) by FINSEQ_1: 40;

          for n st 1 <= n & n <= ( len c) holds (c . n) orientedly_joins ((vs /. n),(vs /. (n + 1))) by A28;

          then vs is_oriented_vertex_seq_of c by A29;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: GRAPH_4:10

    

     Th10: c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c implies vs1 = vs2

    proof

      assume that

       A1: c <> {} and

       A2: vs1 is_oriented_vertex_seq_of c and

       A3: vs2 is_oriented_vertex_seq_of c;

      

       A4: ( len vs1) = (( len c) + 1) by A2;

      

       A5: ( len vs2) = (( len c) + 1) by A3;

      for n be Nat st 1 <= n & n <= ( len vs1) holds (vs1 . n) = (vs2 . n)

      proof

        let n be Nat;

        assume that

         A6: 1 <= n and

         A7: n <= ( len vs1);

        

         A8: n <= (( len c) + 1) by A2, A7;

        per cases ;

          suppose n < (( len c) + 1);

          then

           A9: n <= ( len c) by NAT_1: 13;

          then (c . n) orientedly_joins ((vs1 /. n),(vs1 /. (n + 1))) by A2, A6;

          then

           A10: (the Source of G . (c . n)) = (vs1 /. n);

          (c . n) orientedly_joins ((vs2 /. n),(vs2 /. (n + 1))) by A3, A6, A9;

          then

           A11: (the Source of G . (c . n)) = (vs2 /. n);

          (vs1 . n) = (vs1 /. n) by A6, A7, FINSEQ_4: 15;

          hence thesis by A4, A5, A6, A7, A10, A11, FINSEQ_4: 15;

        end;

          suppose n >= (( len c) + 1);

          then

           A12: n = (( len c) + 1) by A8, XXREAL_0: 1;

          then

           A13: (n - 1) = ( len c);

          

           A14: ( 0 + 1) <= ( len c) by A1, NAT_1: 13;

          then

           A15: (n - 1) = (n -' 1) by A12, NAT_D: 39;

          

           A16: (n -' 1) = ( len c) by A13, A14, NAT_D: 39;

          then (c . (n -' 1)) orientedly_joins ((vs1 /. (n -' 1)),(vs1 /. ((n -' 1) + 1))) by A2, A14;

          then

           A17: (the Target of G . (c . (n -' 1))) = (vs1 /. ((n -' 1) + 1));

          (c . (n -' 1)) orientedly_joins ((vs2 /. (n -' 1)),(vs2 /. ((n -' 1) + 1))) by A3, A14, A16;

          then

           A18: (the Target of G . (c . (n -' 1))) = (vs2 /. ((n -' 1) + 1));

          (vs1 . n) = (vs1 /. n) by A6, A7, FINSEQ_4: 15;

          hence thesis by A4, A5, A6, A7, A15, A17, A18, FINSEQ_4: 15;

        end;

      end;

      hence thesis by A4, A5, FINSEQ_1: 14;

    end;

    definition

      let G, c;

      assume

       A1: c <> {} ;

      :: GRAPH_4:def6

      func oriented-vertex-seq c -> FinSequence of the carrier of G means it is_oriented_vertex_seq_of c;

      existence by Th9;

      uniqueness by A1, Th10;

    end

    theorem :: GRAPH_4:11

    vs is_oriented_vertex_seq_of c & c1 = (c | ( Seg n)) & vs1 = (vs | ( Seg (n + 1))) implies vs1 is_oriented_vertex_seq_of c1

    proof

      assume

       A1: vs is_oriented_vertex_seq_of c;

      then

       A2: ( len vs) = (( len c) + 1);

      assume that

       A3: c1 = (c | ( Seg n)) and

       A4: vs1 = (vs | ( Seg (n + 1)));

      now

        per cases ;

          suppose

           A5: n <= ( len c);

          then

           A6: (n + 1) <= ( len vs) by A2, XREAL_1: 6;

          

           A7: ( len c1) = n by A3, A5, FINSEQ_1: 17;

          

           A8: ( len vs1) = (n + 1) by A4, A6, FINSEQ_1: 17;

          thus ( len vs1) = (( len c1) + 1) by A4, A6, A7, FINSEQ_1: 17;

          let k be Nat;

          assume that

           A9: 1 <= k and

           A10: k <= ( len c1);

          

           A11: k <= ( len c) by A5, A7, A10, XXREAL_0: 2;

          k in ( Seg n) by A7, A9, A10, FINSEQ_1: 1;

          then

           A12: (c1 . k) = (c . k) by A3, FUNCT_1: 49;

          

           A13: k <= ( len vs) by A2, A11, NAT_1: 12;

          

           A14: k <= (n + 1) by A7, A10, NAT_1: 12;

          then

           A15: k in ( Seg (n + 1)) by A9, FINSEQ_1: 1;

          

           A16: 1 <= (k + 1) by NAT_1: 12;

          (k + 1) <= (( len c1) + 1) by A10, XREAL_1: 7;

          then

           A17: (k + 1) in ( Seg (n + 1)) by A7, A16, FINSEQ_1: 1;

          

           A18: (vs1 . k) = (vs . k) by A4, A15, FUNCT_1: 49;

          

           A19: (vs1 . (k + 1)) = (vs . (k + 1)) by A4, A17, FUNCT_1: 49;

          

           A20: (vs /. k) = (vs . k) by A9, A13, FINSEQ_4: 15;

          

           A21: (vs /. (k + 1)) = (vs . (k + 1)) by A2, A11, A16, FINSEQ_4: 15, XREAL_1: 7;

          

           A22: (vs1 /. k) = (vs1 . k) by A8, A9, A14, FINSEQ_4: 15;

          (vs1 /. (k + 1)) = (vs1 . (k + 1)) by A7, A8, A10, A16, FINSEQ_4: 15, XREAL_1: 7;

          hence (c1 . k) orientedly_joins ((vs1 /. k),(vs1 /. (k + 1))) by A1, A9, A11, A12, A18, A19, A20, A21, A22;

        end;

          suppose

           A23: ( len c) <= n;

          then

           A24: ( len vs) <= (n + 1) by A2, XREAL_1: 6;

          

           A25: c1 = c by A3, A23, FINSEQ_2: 20;

          vs1 = vs by A4, A24, FINSEQ_2: 20;

          hence ( len vs1) = (( len c1) + 1) & for k be Nat st 1 <= k & k <= ( len c1) holds (c1 . k) orientedly_joins ((vs1 /. k),(vs1 /. (k + 1))) by A1, A25;

        end;

      end;

      hence thesis;

    end;

    theorem :: GRAPH_4:12

    

     Th12: 1 <= m & m <= n & n <= ( len c) & q = ((m,n) -cut c) implies q is oriented Chain of G

    proof

      assume that

       A1: 1 <= m and

       A2: m <= n and

       A3: n <= ( len c) and

       A4: q = ((m,n) -cut c);

      consider vs such that

       A5: vs is_oriented_vertex_seq_of c by Th9;

      

       A6: ((( len q) + m) - m) = ((n + 1) - m) by A1, A2, A3, A4, FINSEQ_6:def 4;

      reconsider qq = q as Chain of G by A1, A2, A3, A4, GRAPH_2: 41;

      for n st 1 <= n & n < ( len q) holds (the Source of G . (q . (n + 1))) = (the Target of G . (q . n))

      proof

        let k be Nat;

        assume that

         A7: 1 <= k and

         A8: k < ( len q);

        (1 - 1) <= (m - 1) by A1, XREAL_1: 9;

        then (m - 1) = (m -' 1) by XREAL_0:def 2;

        then

        reconsider m1 = (m - 1) as Element of NAT ;

        reconsider i = (m1 + k) as Nat;

        set v1 = (vs /. i);

        set v2 = (vs /. (i + 1));

        ( 0 + 1) <= k by A7;

        then

        consider j such that 0 <= j and

         A9: j < ( len q) and

         A10: k = (j + 1) by A8, FINSEQ_6: 127;

        

         A11: i = (m + j) by A10;

        (i + 1) = (m + (j + 1)) by A10;

        then

         A12: (c . (i + 1)) = (q . (k + 1)) by A1, A2, A3, A4, A8, FINSEQ_6:def 4;

        

         A13: (c . i) = (q . k) by A1, A2, A3, A4, A9, A10, A11, FINSEQ_6:def 4;

        (1 - 1) <= (m - 1) by A1, XREAL_1: 9;

        then

         A14: ( 0 + 1) <= ((m - 1) + k) by A7, XREAL_1: 7;

        i <= ((m - 1) + (n - (m - 1))) by A6, A8, XREAL_1: 6;

        then i <= ( len c) by A3, XXREAL_0: 2;

        then (c . i) orientedly_joins (v1,v2) by A5, A14;

        then

         A15: (the Target of G . (c . i)) = v2;

        

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

        (k + m) < (n + 1) by A6, A8, XREAL_1: 6;

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

        then (m + k) <= ( len c) by A3, XXREAL_0: 2;

        then (c . (i + 1)) orientedly_joins (v2,(vs /. ((i + 1) + 1))) by A5, A16;

        hence thesis by A12, A13, A15;

      end;

      then qq is oriented by GRAPH_1:def 15;

      hence thesis;

    end;

    theorem :: GRAPH_4:13

    

     Th13: 1 <= m & m <= n & n <= ( len c) & c1 = ((m,n) -cut c) & vs is_oriented_vertex_seq_of c & vs1 = ((m,(n + 1)) -cut vs) implies vs1 is_oriented_vertex_seq_of c1

    proof

      assume that

       A1: 1 <= m and

       A2: m <= n and

       A3: n <= ( len c);

      assume

       A4: c1 = ((m,n) -cut c);

      assume that

       A5: vs is_oriented_vertex_seq_of c and

       A6: vs1 = ((m,(n + 1)) -cut vs);

      

       A7: ( len vs) = (( len c) + 1) by A5;

      

       A8: m <= (n + 1) by A2, NAT_1: 12;

      

       A9: (n + 1) <= ( len vs) by A3, A7, XREAL_1: 6;

      

       A10: (( len c1) + m) = (n + 1) by A1, A2, A3, A4, FINSEQ_6:def 4;

      (( len vs1) + m) = ((n + 1) + 1) by A1, A6, A8, A9, FINSEQ_6:def 4;

      hence

       A11: ( len vs1) = (( len c1) + 1) by A10;

      let k be Nat;

      assume that

       A12: 1 <= k and

       A13: k <= ( len c1);

      ( 0 + 1) <= k by A12;

      then

      consider j such that 0 <= j and

       A14: j < ( len c1) and

       A15: k = (j + 1) by A13, FINSEQ_6: 127;

      set i = (m + j);

      set v1 = (vs /. i);

      set v2 = (vs /. (i + 1));

      (m + k) <= (( len c1) + m) by A13, XREAL_1: 7;

      then

       A16: (((m + j) + 1) - 1) <= ((( len c1) + m) - 1) by A15, XREAL_1: 9;

      

       A17: 1 <= i by A1, NAT_1: 12;

      

       A18: i <= ( len c) by A3, A10, A16, XXREAL_0: 2;

      then

       A19: (c . i) orientedly_joins (v1,v2) by A5, A17;

      j < ( len vs1) by A11, A14, NAT_1: 13;

      then

       A20: (vs1 . k) = (vs . i) by A1, A6, A8, A9, A15, FINSEQ_6:def 4;

      

       A21: (j + 1) < ( len vs1) by A11, A14, XREAL_1: 6;

      ((m + j) + 1) = (m + (j + 1));

      then

       A22: (vs1 . (k + 1)) = (vs . (i + 1)) by A1, A6, A8, A9, A15, A21, FINSEQ_6:def 4;

      

       A23: i <= ( len vs) by A7, A18, NAT_1: 12;

      

       A24: 1 <= (i + 1) by NAT_1: 12;

      

       A25: (vs /. i) = (vs . i) by A1, A23, FINSEQ_4: 15, NAT_1: 12;

      

       A26: (vs /. (i + 1)) = (vs . (i + 1)) by A7, A18, A24, FINSEQ_4: 15, XREAL_1: 7;

      ( 0 + 1) = 1;

      then

       A27: 1 <= k by A15, NAT_1: 13;

      

       A28: k <= ( len c1) by A14, A15, NAT_1: 13;

      then

       A29: k <= ( len vs1) by A11, NAT_1: 12;

      

       A30: 1 <= (k + 1) by NAT_1: 12;

      

       A31: (vs1 /. k) = (vs1 . k) by A27, A29, FINSEQ_4: 15;

      (vs1 /. (k + 1)) = (vs1 . (k + 1)) by A11, A28, A30, FINSEQ_4: 15, XREAL_1: 7;

      hence thesis by A1, A2, A3, A4, A14, A15, A19, A20, A22, A25, A26, A31, FINSEQ_6:def 4;

    end;

    theorem :: GRAPH_4:14

    

     Th14: vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & (vs1 . ( len vs1)) = (vs2 . 1) implies (c1 ^ c2) is oriented Chain of G

    proof

      assume that

       A1: vs1 is_oriented_vertex_seq_of c1 and

       A2: vs2 is_oriented_vertex_seq_of c2 and

       A3: (vs1 . ( len vs1)) = (vs2 . 1);

      

       A4: vs1 is_vertex_seq_of c1 by A1, Th4;

      

       A5: vs2 is_vertex_seq_of c2 by A2, Th4;

      

       A6: ( len vs1) = (( len c1) + 1) by A1;

      

       A7: ( len vs2) = (( len c2) + 1) by A2;

      set q = (c1 ^ c2);

      set p = (vs1 ^' vs2);

      thus (c1 ^ c2) is oriented Chain of G

      proof

        reconsider cc = (c1 ^ c2) as Chain of G by A3, A4, A5, GRAPH_2: 43;

        for n st 1 <= n & n < ( len q) holds (the Source of G . (q . (n + 1))) = (the Target of G . (q . n))

        proof

          let n;

          assume that

           A8: 1 <= n and

           A9: n < ( len q);

          

           A10: n in ( dom q) by A8, A9, FINSEQ_3: 25;

          

           A11: (n + 1) <= ( len q) by A9, NAT_1: 13;

          

           A12: 1 < (n + 1) by A8, NAT_1: 13;

          now

            per cases by A10, FINSEQ_1: 25;

              case

               A13: n in ( dom c1);

              then

               A14: (q . n) = (c1 . n) by FINSEQ_1:def 7;

              set v1 = (vs1 /. n);

              set v2 = (vs1 /. (n + 1));

              

               A15: 1 <= n by A13, FINSEQ_3: 25;

              

               A16: n <= ( len c1) by A13, FINSEQ_3: 25;

              then

               A17: (c1 . n) orientedly_joins (v1,v2) by A1, A15;

              

               A18: n <= ( len vs1) by A6, A16, NAT_1: 12;

              (n + 1) <= (( len c1) + 1) by A16, XREAL_1: 6;

              then

               A19: (n + 1) <= ( len vs1) by A1;

              

               A20: (vs1 /. n) = (vs1 . n) by A15, A18, FINSEQ_4: 15;

              

               A21: (vs1 /. (n + 1)) = (vs1 . (n + 1)) by A19, FINSEQ_4: 15, NAT_1: 12;

              

               A22: (p . n) = (vs1 . n) by A15, A18, FINSEQ_6: 140;

              (p . (n + 1)) = (vs1 . (n + 1)) by A19, FINSEQ_6: 140, NAT_1: 12;

              hence ex v1,v2 be Element of G st v1 = (p . n) & v2 = (p . (n + 1)) & (q . n) orientedly_joins (v1,v2) by A14, A17, A20, A21, A22;

            end;

              case ex k be Nat st k in ( dom c2) & n = (( len c1) + k);

              then

              consider k be Nat such that

               A23: k in ( dom c2) and

               A24: n = (( len c1) + k);

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

              

               A25: (q . n) = (c2 . k) by A23, A24, FINSEQ_1:def 7;

              

               A26: 1 <= k by A23, FINSEQ_3: 25;

              

               A27: k <= ( len c2) by A23, FINSEQ_3: 25;

              

               A28: 1 <= (k + 1) by NAT_1: 12;

              

               A29: k <= ( len vs2) by A7, A27, NAT_1: 12;

              set v1 = (vs2 /. k);

              set v2 = (vs2 /. (k + 1));

              

               A30: (vs2 /. k) = (vs2 . k) by A26, A29, FINSEQ_4: 15;

              

               A31: (vs2 /. (k + 1)) = (vs2 . (k + 1)) by A7, A27, A28, FINSEQ_4: 15, XREAL_1: 7;

              

               A32: (c2 . k) orientedly_joins (v1,v2) by A2, A26, A27;

              

               A33: k <= ( len vs2) by A7, A27, NAT_1: 12;

              ( 0 + 1) <= k by A23, FINSEQ_3: 25;

              then

              consider j such that 0 <= j and

               A34: j < ( len vs2) and

               A35: k = (j + 1) by A33, FINSEQ_6: 127;

              

               A36: (p . n) = (vs2 . k)

              proof

                per cases by A26, XXREAL_0: 1;

                  suppose

                   A37: 1 = k;

                  

                   A38: ( 0 + 1) <= ( len vs1) by A6, NAT_1: 13;

                  

                  thus (p . n) = (p . ( len vs1)) by A1, A24, A37

                  .= (vs2 . k) by A3, A37, A38, FINSEQ_6: 140;

                end;

                  suppose 1 < k;

                  then

                   A39: 1 <= j by A35, NAT_1: 13;

                  

                  thus (p . n) = (p . ((( len c1) + 1) + j)) by A24, A35

                  .= (p . (( len vs1) + j)) by A1

                  .= (vs2 . k) by A34, A35, A39, FINSEQ_6: 141;

                end;

              end;

              

               A40: k < ( len vs2) by A7, A27, NAT_1: 13;

              (p . (n + 1)) = (p . ((( len c1) + 1) + k)) by A24

              .= (p . (( len vs1) + k)) by A1

              .= (vs2 . (k + 1)) by A26, A40, FINSEQ_6: 141;

              hence ex v1,v2 be Element of G st v1 = (p . n) & v2 = (p . (n + 1)) & (q . n) orientedly_joins (v1,v2) by A25, A30, A31, A32, A36;

            end;

          end;

          then

          consider v1,v2 be Element of G such that v1 = (p . n) and

           A41: v2 = (p . (n + 1)) and

           A42: (q . n) orientedly_joins (v1,v2);

          

           A43: (n + 1) in ( dom q) by A11, A12, FINSEQ_3: 25;

           A44:

          now

            per cases by A43, FINSEQ_1: 25;

              case

               A45: (n + 1) in ( dom c1);

              then

               A46: (q . (n + 1)) = (c1 . (n + 1)) by FINSEQ_1:def 7;

              set v29 = (vs1 /. (n + 1)), v3 = (vs1 /. ((n + 1) + 1));

              

               A47: 1 <= (n + 1) by A45, FINSEQ_3: 25;

              

               A48: (n + 1) <= ( len c1) by A45, FINSEQ_3: 25;

              then

               A49: (c1 . (n + 1)) orientedly_joins (v29,v3) by A1, A47;

              

               A50: (n + 1) <= ( len vs1) by A6, A48, NAT_1: 12;

              ((n + 1) + 1) <= (( len c1) + 1) by A48, XREAL_1: 6;

              then

               A51: ((n + 1) + 1) <= ( len vs1) by A1;

              

               A52: (vs1 /. (n + 1)) = (vs1 . (n + 1)) by A47, A50, FINSEQ_4: 15;

              

               A53: (vs1 /. ((n + 1) + 1)) = (vs1 . ((n + 1) + 1)) by A51, FINSEQ_4: 15, NAT_1: 12;

              

               A54: (p . (n + 1)) = (vs1 . (n + 1)) by A47, A50, FINSEQ_6: 140;

              (p . ((n + 1) + 1)) = (vs1 . ((n + 1) + 1)) by A51, FINSEQ_6: 140, NAT_1: 12;

              hence ex v299,v39 be Element of G st v299 = (p . (n + 1)) & v39 = (p . ((n + 1) + 1)) & (q . (n + 1)) orientedly_joins (v299,v39) by A46, A49, A52, A53, A54;

            end;

              case ex k be Nat st k in ( dom c2) & (n + 1) = (( len c1) + k);

              then

              consider k be Nat such that

               A55: k in ( dom c2) and

               A56: (n + 1) = (( len c1) + k);

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

              

               A57: (q . (n + 1)) = (c2 . k) by A55, A56, FINSEQ_1:def 7;

              

               A58: 1 <= k by A55, FINSEQ_3: 25;

              

               A59: k <= ( len c2) by A55, FINSEQ_3: 25;

              

               A60: 1 <= (k + 1) by NAT_1: 12;

              

               A61: k <= ( len vs2) by A7, A59, NAT_1: 12;

              set v29 = (vs2 /. k), v3 = (vs2 /. (k + 1));

              

               A62: (vs2 /. k) = (vs2 . k) by A58, A61, FINSEQ_4: 15;

              

               A63: (vs2 /. (k + 1)) = (vs2 . (k + 1)) by A7, A59, A60, FINSEQ_4: 15, XREAL_1: 7;

              

               A64: (c2 . k) orientedly_joins (v29,v3) by A2, A58, A59;

              

               A65: k <= ( len vs2) by A7, A59, NAT_1: 12;

              ( 0 + 1) <= k by A55, FINSEQ_3: 25;

              then

              consider j such that 0 <= j and

               A66: j < ( len vs2) and

               A67: k = (j + 1) by A65, FINSEQ_6: 127;

              

               A68: (p . (n + 1)) = (vs2 . k)

              proof

                per cases by A58, XXREAL_0: 1;

                  suppose

                   A69: 1 = k;

                  

                   A70: ( 0 + 1) <= ( len vs1) by A6, NAT_1: 13;

                  

                  thus (p . (n + 1)) = (p . ( len vs1)) by A1, A56, A69

                  .= (vs2 . k) by A3, A69, A70, FINSEQ_6: 140;

                end;

                  suppose 1 < k;

                  then

                   A71: 1 <= j by A67, NAT_1: 13;

                  

                  thus (p . (n + 1)) = (p . ((( len c1) + 1) + j)) by A56, A67

                  .= (p . (( len vs1) + j)) by A1

                  .= (vs2 . k) by A66, A67, A71, FINSEQ_6: 141;

                end;

              end;

              

               A72: k < ( len vs2) by A7, A59, NAT_1: 13;

              (p . ((n + 1) + 1)) = (p . ((( len c1) + 1) + k)) by A56

              .= (p . (( len vs1) + k)) by A1

              .= (vs2 . (k + 1)) by A58, A72, FINSEQ_6: 141;

              hence ex v299,v39 be Element of G st v299 = (p . (n + 1)) & v39 = (p . ((n + 1) + 1)) & (q . (n + 1)) orientedly_joins (v299,v39) by A57, A62, A63, A64, A68;

            end;

          end;

          (the Target of G . (q . n)) = v2 by A42;

          hence thesis by A41, A44;

        end;

        then cc is oriented by GRAPH_1:def 15;

        hence thesis;

      end;

    end;

    theorem :: GRAPH_4:15

    

     Th15: vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & (vs1 . ( len vs1)) = (vs2 . 1) & c = (c1 ^ c2) & vs = (vs1 ^' vs2) implies vs is_oriented_vertex_seq_of c

    proof

      assume that

       A1: vs1 is_oriented_vertex_seq_of c1 and

       A2: vs2 is_oriented_vertex_seq_of c2 and

       A3: (vs1 . ( len vs1)) = (vs2 . 1);

      assume that

       A4: c = (c1 ^ c2) and

       A5: vs = (vs1 ^' vs2);

      

       A6: ( len vs1) = (( len c1) + 1) by A1;

      

       A7: ( len vs2) = (( len c2) + 1) by A2;

      then

       A8: vs2 <> {} ;

      set q = (c1 ^ c2);

      set p = (vs1 ^' vs2);

      (( len p) + 1) = (( len vs1) + ( len vs2)) by A8, FINSEQ_6: 139;

      

      then

       A9: ( len p) = ((( len c1) + ( len c2)) + 1) by A6, A7

      .= (( len q) + 1) by FINSEQ_1: 22;

      reconsider p as FinSequence of the carrier of G;

      now

        let n be Nat;

        assume that

         A10: 1 <= n and

         A11: n <= ( len q);

        

         A12: n <= ( len p) by A9, A11, NAT_1: 12;

        

         A13: 1 <= (n + 1) by NAT_1: 12;

        

         A14: (p /. n) = (p . n) by A10, A12, FINSEQ_4: 15;

        

         A15: (p /. (n + 1)) = (p . (n + 1)) by A9, A11, A13, FINSEQ_4: 15, XREAL_1: 7;

        

         A16: n in ( dom q) by A10, A11, FINSEQ_3: 25;

        per cases by A16, FINSEQ_1: 25;

          suppose

           A17: n in ( dom c1);

          set v1 = (vs1 /. n);

          set v2 = (vs1 /. (n + 1));

          

           A18: 1 <= n by A17, FINSEQ_3: 25;

          

           A19: n <= ( len c1) by A17, FINSEQ_3: 25;

          then

           A20: (c1 . n) orientedly_joins (v1,v2) by A1, A18;

          

           A21: n <= ( len vs1) by A6, A19, NAT_1: 12;

          (n + 1) <= (( len c1) + 1) by A19, XREAL_1: 6;

          then

           A22: (n + 1) <= ( len vs1) by A1;

          

           A23: (vs1 /. n) = (vs1 . n) by A18, A21, FINSEQ_4: 15;

          

           A24: (vs1 /. (n + 1)) = (vs1 . (n + 1)) by A22, FINSEQ_4: 15, NAT_1: 12;

          

           A25: (p . n) = (vs1 . n) by A18, A21, FINSEQ_6: 140;

          (p . (n + 1)) = (vs1 . (n + 1)) by A22, FINSEQ_6: 140, NAT_1: 12;

          hence (q . n) orientedly_joins ((p /. n),(p /. (n + 1))) by A14, A15, A17, A20, A23, A24, A25, FINSEQ_1:def 7;

        end;

          suppose ex k be Nat st k in ( dom c2) & n = (( len c1) + k);

          then

          consider k be Nat such that

           A26: k in ( dom c2) and

           A27: n = (( len c1) + k);

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

          

           A28: (q . n) = (c2 . k) by A26, A27, FINSEQ_1:def 7;

          

           A29: 1 <= k by A26, FINSEQ_3: 25;

          

           A30: k <= ( len c2) by A26, FINSEQ_3: 25;

          

           A31: 1 <= (k + 1) by NAT_1: 12;

          k <= ( len vs2) by A7, A30, NAT_1: 12;

          then

           A32: (vs2 /. k) = (vs2 . k) by A29, FINSEQ_4: 15;

          

           A33: (vs2 /. (k + 1)) = (vs2 . (k + 1)) by A7, A30, A31, FINSEQ_4: 15, XREAL_1: 7;

          

           A34: k <= ( len vs2) by A7, A30, NAT_1: 12;

          ( 0 + 1) <= k by A26, FINSEQ_3: 25;

          then

          consider j such that 0 <= j and

           A35: j < ( len vs2) and

           A36: k = (j + 1) by A34, FINSEQ_6: 127;

          

           A37: (p . n) = (vs2 . k)

          proof

            per cases by A29, XXREAL_0: 1;

              suppose

               A38: 1 = k;

              

               A39: ( 0 + 1) <= ( len vs1) by A6, NAT_1: 13;

              

              thus (p . n) = (p . ( len vs1)) by A1, A27, A38

              .= (vs2 . k) by A3, A38, A39, FINSEQ_6: 140;

            end;

              suppose 1 < k;

              then

               A40: 1 <= j by A36, NAT_1: 13;

              

              thus (p . n) = (p . ((( len c1) + 1) + j)) by A27, A36

              .= (p . (( len vs1) + j)) by A1

              .= (vs2 . k) by A35, A36, A40, FINSEQ_6: 141;

            end;

          end;

          

           A41: k < ( len vs2) by A7, A30, NAT_1: 13;

          (p . (n + 1)) = (p . ((( len c1) + 1) + k)) by A27

          .= (p . (( len vs1) + k)) by A1

          .= (vs2 . (k + 1)) by A29, A41, FINSEQ_6: 141;

          hence (q . n) orientedly_joins ((p /. n),(p /. (n + 1))) by A2, A14, A15, A28, A29, A30, A32, A33, A37;

        end;

      end;

      hence thesis by A4, A5, A9;

    end;

    begin

    

     Lm1: <*v*> is_oriented_vertex_seq_of {} by FINSEQ_1: 39;

    definition

      let G;

      let IT be oriented Chain of G;

      :: GRAPH_4:def7

      attr IT is Simple means

      : Def7: ex vs st vs is_oriented_vertex_seq_of IT & for n, m st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs);

    end

    registration

      let G;

      cluster Simple for oriented Chain of G;

      existence

      proof

        set q = the empty oriented Chain of G;

        set x = the Element of G;

        reconsider p = <*x*> as FinSequence of the carrier of G;

        

         A1: p is_oriented_vertex_seq_of q by Lm1;

        for n, m st 1 <= n & n < m & m <= ( len p) & (p . n) = (p . m) holds n = 1 & m = ( len p)

        proof

          let n, m;

          assume that

           A2: 1 <= n and

           A3: n < m and

           A4: m <= ( len p) and (p . n) = (p . m);

          1 < m by A2, A3, XXREAL_0: 2;

          hence thesis by A4, FINSEQ_1: 39;

        end;

        then q is Simple by A1;

        hence thesis;

      end;

    end

    registration

      let G;

      cluster oriented simple for Chain of G;

      existence

      proof

        set q = the empty oriented Chain of G;

        set x = the Element of G;

        reconsider p = <*x*> as FinSequence of the carrier of G;

        

         A1: p is_vertex_seq_of q by Lm1, Th4;

        reconsider q9 = q as Chain of G;

        for n, m st 1 <= n & n < m & m <= ( len p) & (p . n) = (p . m) holds n = 1 & m = ( len p)

        proof

          let n, m;

          assume that

           A2: 1 <= n and

           A3: n < m and

           A4: m <= ( len p) and (p . n) = (p . m);

          1 < m by A2, A3, XXREAL_0: 2;

          hence thesis by A4, FINSEQ_1: 39;

        end;

        then q9 is simple by A1, GRAPH_2:def 9;

        hence thesis;

      end;

    end

    theorem :: GRAPH_4:16

    

     Th16: for q be oriented Chain of G holds (q | ( Seg n)) is oriented Chain of G

    proof

      let q be oriented Chain of G;

      reconsider q9 = (q | ( Seg n)) as FinSequence;

      for i st 1 <= i & i < ( len q9) holds (the Source of G . ((q | ( Seg n)) . (i + 1))) = (the Target of G . ((q | ( Seg n)) . i))

      proof

        let i;

        assume that

         A1: 1 <= i and

         A2: i < ( len q9);

        per cases ;

          suppose n >= ( len q);

          then (q | ( Seg n)) = q by FINSEQ_3: 49;

          hence thesis by A1, A2, GRAPH_1:def 15;

        end;

          suppose

           A3: n < ( len q);

          then

           A4: ( len q9) = n by FINSEQ_1: 17;

          then

           A5: i < ( len q) by A2, A3, XXREAL_0: 2;

          i in ( Seg n) by A1, A2, A4, FINSEQ_1: 1;

          then

           A6: ((q | ( Seg n)) . i) = (q . i) by FUNCT_1: 49;

          

           A7: (i + 1) <= n by A2, A4, NAT_1: 13;

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

          then (i + 1) in ( Seg n) by A7, FINSEQ_1: 1;

          then ((q | ( Seg n)) . (i + 1)) = (q . (i + 1)) by FUNCT_1: 49;

          hence thesis by A1, A5, A6, GRAPH_1:def 15;

        end;

      end;

      hence thesis by GRAPH_1: 4, GRAPH_1:def 15;

    end;

    reserve sc for oriented simple Chain of G;

    theorem :: GRAPH_4:17

    (sc | ( Seg n)) is oriented simple Chain of G by Th16, GRAPH_2: 45;

    theorem :: GRAPH_4:18

    

     Th18: for sc9 be oriented Chain of G st sc9 = sc holds sc9 is Simple

    proof

      let sc9 be oriented Chain of G;

      assume

       A1: sc9 = sc;

      consider vs such that

       A2: vs is_oriented_vertex_seq_of sc9 by Th9;

      vs is_vertex_seq_of sc by A1, A2, Th4;

      then for n, m st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs) by GRAPH_2: 47;

      hence thesis by A2;

    end;

    theorem :: GRAPH_4:19

    

     Th19: for sc9 be Simple oriented Chain of G holds sc9 is oriented simple Chain of G

    proof

      let sc9 be Simple oriented Chain of G;

      consider vs such that

       A1: vs is_oriented_vertex_seq_of sc9 and

       A2: for n, m st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs) by Def7;

      vs is_vertex_seq_of sc9 by A1, Th4;

      hence thesis by A2, GRAPH_2:def 9;

    end;

    reserve x,y for set;

    

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

    proof

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

       A1: 1 <= m and

       A2: m <= (n + 1) and

       A3: n <= ( len p);

      

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

      per cases by A4, NAT_1: 13;

        suppose

         A5: m = (n + 1);

        then

         A6: n < m by XREAL_1: 29;

        

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

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

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

        thus thesis by A7, CARD_1: 27, FINSEQ_6:def 4;

      end;

        suppose m <= n;

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

      end;

    end;

    theorem :: GRAPH_4:20

    

     Th20: not c is Simple & vs is_oriented_vertex_seq_of c implies ex fc be Subset of c, fvs be Subset of vs, c1, vs1 st ( len c1) < ( len c) & vs1 is_oriented_vertex_seq_of c1 & ( len vs1) < ( len vs) & (vs . 1) = (vs1 . 1) & (vs . ( len vs)) = (vs1 . ( len vs1)) & ( Seq fc) = c1 & ( Seq fvs) = vs1

    proof

      assume that

       A1: not c is Simple and

       A2: vs is_oriented_vertex_seq_of c;

      consider n,m be Nat such that

       A3: 1 <= n and

       A4: n < m and

       A5: m <= ( len vs) and

       A6: (vs . n) = (vs . m) and

       A7: n <> 1 or m <> ( len vs) by A1, A2;

      

       A8: ( len vs) = (( len c) + 1) by A2;

      

       A9: (m - n) > (n - n) by A4, XREAL_1: 9;

      reconsider n1 = (n -' 1) as Element of NAT ;

      

       A10: (1 - 1) <= (n - 1) by A3, XREAL_1: 9;

      then

       A11: (n - 1) = (n -' 1) by XREAL_0:def 2;

      

       A12: (n1 + 1) = ((n - 1) + 1) by A10, XREAL_0:def 2

      .= n;

      per cases by A7;

        suppose

         A13: n <> 1 & m <> ( len vs);

        then 1 < n by A3, XXREAL_0: 1;

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

        then

         A14: ((1 + 1) - 1) <= (n - 1) by XREAL_1: 9;

        n < ( len vs) by A4, A5, XXREAL_0: 2;

        then

         A15: (n - 1) < ((( len c) + 1) - 1) by A8, XREAL_1: 9;

        

         A16: 1 <= (n1 + 1) by NAT_1: 12;

        

         A17: m < ( len vs) by A5, A13, XXREAL_0: 1;

        then

         A18: m <= ( len c) by A8, NAT_1: 13;

        

         A19: 1 <= m by A3, A4, XXREAL_0: 2;

        

         A20: m <= ( len c) by A8, A17, NAT_1: 13;

        reconsider c1 = ((1,n1) -cut c) as oriented Chain of G by A11, A14, A15, Th12;

        reconsider c2 = ((m,( len c)) -cut c) as oriented Chain of G by A19, A20, Th12;

        set pp = ((1,n) -cut vs);

        set p2 = ((m,(( len c) + 1)) -cut vs);

        set p29 = (((m + 1),(( len c) + 1)) -cut vs);

        reconsider pp as FinSequence of the carrier of G;

        reconsider p2 as FinSequence of the carrier of G;

        

         A21: n <= ( len vs) by A4, A5, XXREAL_0: 2;

        

         A22: 1 <= m by A3, A4, XXREAL_0: 2;

        

         A23: m <= (( len c) + 1) by A2, A5;

        

         A24: (( len c) + 1) <= ( len vs) by A2;

        

         A25: pp is_oriented_vertex_seq_of c1 by A2, A12, A14, A15, Th13;

        

         A26: p2 is_oriented_vertex_seq_of c2 by A2, A19, A20, Th13;

        

         A27: ( len pp) = (( len c1) + 1) by A25;

        

         A28: ( len p2) = (( len c2) + 1) by A26;

        (1 - 1) <= (m - 1) by A19, XREAL_1: 9;

        then (m -' 1) = (m - 1) by XREAL_0:def 2;

        then

        reconsider m1 = (m - 1) as Element of NAT ;

        

         A29: m = (m1 + 1);

        

         A30: (( len c2) + m) = (( len c) + 1) by A19, A20, FINSEQ_6:def 4;

        

         A31: (m - m) <= (( len c) - m) by A18, XREAL_1: 9;

        then (( len c2) -' 1) = (( len c2) - 1) by A30, XREAL_0:def 2;

        then

        reconsider lc21 = (( len c2) - 1) as Element of NAT ;

        

         A32: (m + lc21) = (m1 + ( len c2));

        ( 0 + 1) = 1;

        then

         A33: 1 <= ( len p2) by A28, NAT_1: 13;

        

         A34: p2 = ((( 0 + 1),( len p2)) -cut p2) by FINSEQ_6: 133

        .= (((( 0 + 1),1) -cut p2) ^ (((1 + 1),( len p2)) -cut p2)) by A33, FINSEQ_6: 134;

        m1 <= m by A29, NAT_1: 12;

        then

         A35: p2 = ((((m1 + 1),m) -cut vs) ^ (((m + 1),(( len c) + 1)) -cut vs)) by A5, A8, FINSEQ_6: 134;

        ((1,1) -cut p2) = <*(p2 . ( 0 + 1))*> by A33, FINSEQ_6: 132

        .= <*(vs . (m + 0 ))*> by A22, A23, A24, A28, FINSEQ_6:def 4

        .= ((m,m) -cut vs) by A5, A19, FINSEQ_6: 132;

        then

         A36: p29 = ((2,( len p2)) -cut p2) by A34, A35, FINSEQ_1: 33;

        set domfc = { k where k be Nat : 1 <= k & k <= n1 or m <= k & k <= ( len c) };

        deffunc F( object) = (c . $1);

        consider fc be Function such that

         A37: ( dom fc) = domfc and

         A38: for x be object st x in domfc holds (fc . x) = F(x) from FUNCT_1:sch 3;

        domfc c= ( Seg ( len c))

        proof

          let x be object;

          assume x in domfc;

          then

          consider kk be Nat such that

           A39: x = kk and

           A40: 1 <= kk & kk <= n1 or m <= kk & kk <= ( len c);

          

           A41: 1 <= kk by A19, A40, XXREAL_0: 2;

          kk <= ( len c) by A11, A15, A40, XXREAL_0: 2;

          hence thesis by A39, A41, FINSEQ_1: 1;

        end;

        then

        reconsider fc as FinSubsequence by A37, FINSEQ_1:def 12;

        fc c= c

        proof

          let p be object;

          assume

           A42: p in fc;

          then

          consider x,y be object such that

           A43: [x, y] = p by RELAT_1:def 1;

          

           A44: x in ( dom fc) by A42, A43, FUNCT_1: 1;

          

           A45: y = (fc . x) by A42, A43, FUNCT_1: 1;

          consider kk be Nat such that

           A46: x = kk and

           A47: 1 <= kk & kk <= n1 or m <= kk & kk <= ( len c) by A37, A44;

          

           A48: 1 <= kk by A19, A47, XXREAL_0: 2;

          kk <= ( len c) by A11, A15, A47, XXREAL_0: 2;

          then

           A49: x in ( dom c) by A46, A48, FINSEQ_3: 25;

          y = (c . kk) by A37, A38, A44, A45, A46;

          hence thesis by A43, A46, A49, FUNCT_1: 1;

        end;

        then

        reconsider fc as Subset of c;

        take fc;

        set domfvs = { k where k be Nat : 1 <= k & k <= n or (m + 1) <= k & k <= ( len vs) };

        deffunc F( object) = (vs . $1);

        consider fvs be Function such that

         A50: ( dom fvs) = domfvs and

         A51: for x be object st x in domfvs holds (fvs . x) = F(x) from FUNCT_1:sch 3;

        domfvs c= ( Seg ( len vs))

        proof

          let x be object;

          assume x in domfvs;

          then

          consider kk be Nat such that

           A52: x = kk and

           A53: 1 <= kk & kk <= n or (m + 1) <= kk & kk <= ( len vs);

          1 <= (m + 1) by NAT_1: 12;

          then

           A54: 1 <= kk by A53, XXREAL_0: 2;

          kk <= ( len vs) by A21, A53, XXREAL_0: 2;

          hence thesis by A52, A54, FINSEQ_1: 1;

        end;

        then

        reconsider fvs as FinSubsequence by A50, FINSEQ_1:def 12;

        fvs c= vs

        proof

          let p be object;

          assume

           A55: p in fvs;

          then

          consider x,y be object such that

           A56: [x, y] = p by RELAT_1:def 1;

          

           A57: x in ( dom fvs) by A55, A56, FUNCT_1: 1;

          

           A58: y = (fvs . x) by A55, A56, FUNCT_1: 1;

          consider kk be Nat such that

           A59: x = kk and

           A60: 1 <= kk & kk <= n or (m + 1) <= kk & kk <= ( len vs) by A50, A57;

          1 <= (m + 1) by NAT_1: 12;

          then

           A61: 1 <= kk by A60, XXREAL_0: 2;

          kk <= ( len vs) by A21, A60, XXREAL_0: 2;

          then

           A62: x in ( dom vs) by A59, A61, FINSEQ_3: 25;

          y = (vs . kk) by A50, A51, A57, A58, A59;

          hence thesis by A56, A59, A62, FUNCT_1: 1;

        end;

        then

        reconsider fvs as Subset of vs;

        take fvs;

        

         A63: (p2 . 1) = (vs . m) by A22, A23, A24, FINSEQ_6: 138;

        

         A64: (pp . ( len pp)) = (vs . n) by A3, A21, FINSEQ_6: 138;

        then

        reconsider c9 = (c1 ^ c2) as oriented Chain of G by A6, A25, A26, A63, Th14;

        take c9;

        take p1 = (pp ^' p2);

        

         A65: p1 = (pp ^ p29) by A36, FINSEQ_6:def 5;

        

         A66: (( len c1) + 1) = (n1 + 1) by A11, A15, A16, Lm2;

        ( - ( - (m - n))) = (m - n);

        then

         A67: ( - (m - n)) < 0 by A9;

        ( len c9) = ((n - 1) + ((( len c) - m) + 1)) by A11, A30, A66, FINSEQ_1: 22

        .= (( len c) + (n + ( - m)));

        hence

         A68: ( len c9) < ( len c) by A67, XREAL_1: 30;

        thus p1 is_oriented_vertex_seq_of c9 by A6, A25, A26, A63, A64, Th15;

        then ( len p1) = (( len c9) + 1);

        hence ( len p1) < ( len vs) by A8, A68, XREAL_1: 6;

        1 <= (1 + ( len c1)) by NAT_1: 12;

        then 1 <= ( len pp) by A25;

        then (p1 . 1) = (pp . 1) by FINSEQ_6: 140;

        hence (vs . 1) = (p1 . 1) by A3, A21, FINSEQ_6: 138;

        

         A69: (p2 . ( len p2)) = (vs . (( len c) + 1)) by A22, A23, A24, FINSEQ_6: 138;

        (m - m) <= (( len c) - m) by A20, XREAL_1: 9;

        then ( 0 + 1) <= ((( len c) - m) + 1) by XREAL_1: 6;

        then 1 < ( len p2) by A28, A30, NAT_1: 13;

        hence (vs . ( len vs)) = (p1 . ( len p1)) by A8, A69, FINSEQ_6: 142;

        set DL = { kk where kk be Nat : 1 <= kk & kk <= n1 };

        set DR = { kk where kk be Nat : m <= kk & kk <= ( len c) };

        now

          let x be object;

          hereby

            assume x in domfc;

            then ex k be Nat st (x = k) & (1 <= k & k <= n1 or m <= k & k <= ( len c));

            then x in DL or x in DR;

            hence x in (DL \/ DR) by XBOOLE_0:def 3;

          end;

          assume

           A70: x in (DL \/ DR);

          per cases by A70, XBOOLE_0:def 3;

            suppose x in DL;

            then ex k be Nat st (x = k) & (1 <= k) & (k <= n1);

            hence x in domfc;

          end;

            suppose x in DR;

            then ex k be Nat st (x = k) & (m <= k) & (k <= ( len c));

            hence x in domfc;

          end;

        end;

        then

         A71: domfc = (DL \/ DR) by TARSKI: 2;

        

         A72: DL c= ( Seg ( len c)) & DR c= ( Seg ( len c))

        proof

          hereby

            let x be object;

            assume x in DL;

            then

            consider k be Nat such that

             A73: x = k and

             A74: 1 <= k and

             A75: k <= n1;

            k <= ( len c) by A11, A15, A75, XXREAL_0: 2;

            hence x in ( Seg ( len c)) by A73, A74, FINSEQ_1: 1;

          end;

          let x be object;

          assume x in DR;

          then

          consider k be Nat such that

           A76: x = k and

           A77: m <= k and

           A78: k <= ( len c);

          1 <= k by A22, A77, XXREAL_0: 2;

          hence thesis by A76, A78, FINSEQ_1: 1;

        end;

        then

        reconsider DL as finite set by FINSET_1: 1;

        reconsider DR as finite set by A72, FINSET_1: 1;

        now

          let i, j;

          assume i in DL;

          then

          consider k be Nat such that

           A79: k = i and 1 <= k and

           A80: k <= n1;

          assume j in DR;

          then

           A81: ex l be Nat st (l = j) & (m <= l) & (l <= ( len c));

          n1 < m by A4, A12, NAT_1: 13;

          then k < m by A80, XXREAL_0: 2;

          hence i < j by A79, A81, XXREAL_0: 2;

        end;

        then

         A82: ( Sgm (DL \/ DR)) = (( Sgm DL) ^ ( Sgm DR)) by A72, FINSEQ_3: 42;

        (m + lc21) = ( len c) by A30;

        

        then

         A83: ( card DR) = ((( len c2) + ( - 1)) + 1) by FINSEQ_6: 130

        .= ( len c2);

        

         A84: ( len ( Sgm DR)) = ( card DR) by A72, FINSEQ_3: 39;

        DL = ( Seg n1) by FINSEQ_1:def 1;

        then

         A85: ( Sgm DL) = ( idseq n1) by FINSEQ_3: 48;

        then

         A86: ( dom ( Sgm DL)) = ( Seg n1);

        ( rng ( Sgm DL)) = DL by A72, FINSEQ_1:def 13;

        then

         A87: ( rng ( Sgm DL)) c= ( dom fc) by A37, A71, XBOOLE_1: 7;

        ( rng ( Sgm DR)) = DR by A72, FINSEQ_1:def 13;

        then

         A88: ( rng ( Sgm DR)) c= ( dom fc) by A37, A71, XBOOLE_1: 7;

        set SL = ( Sgm DL);

        set SR = ( Sgm DR);

        now

          let p be object;

          hereby

            assume

             A89: p in c1;

            then

            consider x,y be object such that

             A90: p = [x, y] by RELAT_1:def 1;

            

             A91: x in ( dom c1) by A89, A90, FUNCT_1: 1;

            

             A92: y = (c1 . x) by A89, A90, FUNCT_1: 1;

            reconsider k = x as Element of NAT by A91;

            

             A93: 1 <= k by A91, FINSEQ_3: 25;

            

             A94: k <= ( len c1) by A91, FINSEQ_3: 25;

            then

             A95: x in ( dom SL) by A66, A86, A93, FINSEQ_1: 1;

            then

             A96: k = (SL . k) by A85, FUNCT_1: 18;

            

             A97: k in domfc by A66, A93, A94;

            then

             A98: x in ( dom (fc * SL)) by A37, A95, A96, FUNCT_1: 11;

            ( 0 + 1) <= k by A91, FINSEQ_3: 25;

            then

            consider i be Nat such that 0 <= i and

             A99: i < n1 and

             A100: k = (i + 1) by A66, A94, FINSEQ_6: 127;

            ((fc * SL) . x) = (fc . k) by A96, A98, FUNCT_1: 12

            .= (c . (1 + i)) by A37, A97, A100, GRFUNC_1: 2

            .= y by A11, A15, A16, A66, A92, A99, A100, Lm2;

            hence p in (fc * ( Sgm DL)) by A90, A98, FUNCT_1: 1;

          end;

          assume

           A101: p in (fc * ( Sgm DL));

          then

          consider x,y be object such that

           A102: p = [x, y] by RELAT_1:def 1;

          

           A103: x in ( dom (fc * SL)) by A101, A102, FUNCT_1: 1;

          

           A104: y = ((fc * SL) . x) by A101, A102, FUNCT_1: 1;

          

           A105: ((fc * SL) . x) = (fc . (SL . x)) by A103, FUNCT_1: 12;

          

           A106: x in ( dom SL) by A103, FUNCT_1: 11;

          then x in { kk where kk be Nat : 1 <= kk & kk <= n1 } by A86, FINSEQ_1:def 1;

          then

          consider k be Nat such that

           A107: k = x and

           A108: 1 <= k and

           A109: k <= n1;

          

           A110: k in ( dom fc) by A37, A108, A109;

          

           A111: k = (SL . k) by A85, A106, A107, FUNCT_1: 18;

          

           A112: k in ( dom c1) by A66, A108, A109, FINSEQ_3: 25;

          ( 0 + 1) <= k by A108;

          then ex i be Nat st ( 0 <= i) & (i < n1) & (k = (i + 1)) by A109, FINSEQ_6: 127;

          

          then (c1 . k) = (c . k) by A11, A15, A16, A66, Lm2

          .= y by A104, A105, A107, A110, A111, GRFUNC_1: 2;

          hence p in c1 by A102, A107, A112, FUNCT_1: 1;

        end;

        then

         A113: c1 = (fc * ( Sgm DL)) by TARSKI: 2;

        now

          let p be object;

          hereby

            assume

             A114: p in c2;

            then

            consider x,y be object such that

             A115: p = [x, y] by RELAT_1:def 1;

            

             A116: x in ( dom c2) by A114, A115, FUNCT_1: 1;

            

             A117: y = (c2 . x) by A114, A115, FUNCT_1: 1;

            reconsider k = x as Element of NAT by A116;

            

             A118: 1 <= k by A116, FINSEQ_3: 25;

            

             A119: k <= ( len c2) by A116, FINSEQ_3: 25;

            

             A120: x in ( dom SR) by A83, A84, A116, FINSEQ_3: 29;

            

             A121: (m1 + k) = (SR . k) by A29, A30, A32, A118, A119, FINSEQ_6: 131;

            

             A122: (SR . k) in ( rng SR) by A120, FUNCT_1:def 3;

            then

             A123: x in ( dom (fc * SR)) by A88, A120, FUNCT_1: 11;

            ( 0 + 1) <= k by A116, FINSEQ_3: 25;

            then

            consider i be Nat such that 0 <= i and

             A124: i < ( len c2) and

             A125: k = (i + 1) by A119, FINSEQ_6: 127;

            ((fc * SR) . x) = (fc . (m1 + k)) by A121, A123, FUNCT_1: 12

            .= (c . (m + i)) by A88, A121, A122, A125, GRFUNC_1: 2

            .= y by A19, A20, A117, A124, A125, FINSEQ_6:def 4;

            hence p in (fc * ( Sgm DR)) by A115, A123, FUNCT_1: 1;

          end;

          assume

           A126: p in (fc * ( Sgm DR));

          then

          consider x,y be object such that

           A127: p = [x, y] by RELAT_1:def 1;

          

           A128: x in ( dom (fc * SR)) by A126, A127, FUNCT_1: 1;

          

           A129: y = ((fc * SR) . x) by A126, A127, FUNCT_1: 1;

          

           A130: x in ( dom SR) by A128, FUNCT_1: 11;

          

           A131: (SR . x) in ( dom fc) by A128, FUNCT_1: 11;

          reconsider k = x as Element of NAT by A130;

          

           A132: k in ( dom c2) by A83, A84, A130, FINSEQ_3: 29;

          

           A133: 1 <= k by A130, FINSEQ_3: 25;

          

           A134: k <= ( len c2) by A83, A84, A130, FINSEQ_3: 25;

          then

           A135: (m1 + k) = (SR . k) by A29, A30, A32, A133, FINSEQ_6: 131;

          ( 0 + 1) <= k by A130, FINSEQ_3: 25;

          then

          consider i be Nat such that 0 <= i and

           A136: i < ( len c2) and

           A137: k = (i + 1) by A134, FINSEQ_6: 127;

          (c2 . k) = (c . ((m1 + 1) + i)) by A19, A20, A136, A137, FINSEQ_6:def 4

          .= (fc . (SR . k)) by A131, A135, A137, GRFUNC_1: 2

          .= y by A129, A130, FUNCT_1: 13;

          hence p in c2 by A127, A132, FUNCT_1: 1;

        end;

        then

         A138: c2 = (fc * ( Sgm DR)) by TARSKI: 2;

        ( Seq fc) = (fc * (( Sgm DL) ^ ( Sgm DR))) by A37, A71, A82, FINSEQ_1:def 14;

        hence ( Seq fc) = c9 by A87, A88, A113, A138, FINSEQ_6: 150;

        set DL = { kk where kk be Nat : 1 <= kk & kk <= n };

        set DR = { kk where kk be Nat : (m + 1) <= kk & kk <= ( len vs) };

        now

          let x be object;

          hereby

            assume x in domfvs;

            then ex k be Nat st (x = k) & (1 <= k & k <= n or (m + 1) <= k & k <= ( len vs));

            then x in DL or x in DR;

            hence x in (DL \/ DR) by XBOOLE_0:def 3;

          end;

          assume

           A139: x in (DL \/ DR);

          per cases by A139, XBOOLE_0:def 3;

            suppose x in DL;

            then ex k be Nat st (x = k) & (1 <= k) & (k <= n);

            hence x in domfvs;

          end;

            suppose x in DR;

            then ex k be Nat st (x = k) & ((m + 1) <= k) & (k <= ( len vs));

            hence x in domfvs;

          end;

        end;

        then

         A140: domfvs = (DL \/ DR) by TARSKI: 2;

        

         A141: DL c= ( Seg ( len vs)) & DR c= ( Seg ( len vs))

        proof

          hereby

            let x be object;

            assume x in DL;

            then

            consider k be Nat such that

             A142: x = k and

             A143: 1 <= k and

             A144: k <= n;

            k <= ( len vs) by A21, A144, XXREAL_0: 2;

            hence x in ( Seg ( len vs)) by A142, A143, FINSEQ_1: 1;

          end;

          let x be object;

          assume x in DR;

          then

          consider k be Nat such that

           A145: x = k and

           A146: (m + 1) <= k and

           A147: k <= ( len vs);

          1 <= (m + 1) by NAT_1: 12;

          then 1 <= k by A146, XXREAL_0: 2;

          hence thesis by A145, A147, FINSEQ_1: 1;

        end;

        then

        reconsider DL as finite set by FINSET_1: 1;

        reconsider DR as finite set by A141, FINSET_1: 1;

        now

          let i, j;

          assume i in DL;

          then

          consider k be Nat such that

           A148: k = i and 1 <= k and

           A149: k <= n;

          assume j in DR;

          then

          consider l be Nat such that

           A150: l = j and

           A151: (m + 1) <= l and l <= ( len vs);

          m <= (m + 1) by NAT_1: 12;

          then

           A152: m <= l by A151, XXREAL_0: 2;

          k < m by A4, A149, XXREAL_0: 2;

          hence i < j by A148, A150, A152, XXREAL_0: 2;

        end;

        then

         A153: ( Sgm (DL \/ DR)) = (( Sgm DL) ^ ( Sgm DR)) by A141, FINSEQ_3: 42;

        1 <= ( len p2) by A28, NAT_1: 12;

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

        then (( len p2) -' 1) = (( len p2) - 1) by XREAL_0:def 2;

        then

        reconsider lp21 = (( len p2) - 1) as Element of NAT ;

        (lp21 -' 1) = (lp21 - 1) by A28, A30, A31, XREAL_0:def 2;

        then

        reconsider lp22 = (lp21 - 1) as Element of NAT ;

        

         A154: ((m + 1) + lp22) = (m + ((lp21 - 1) + 1))

        .= (m + ((((( len c) - m) + 1) + 1) - 1)) by A26, A30

        .= (( len c) + 1);

        

        then

         A155: ( card DR) = (lp22 + 1) by A8, FINSEQ_6: 130

        .= lp21;

        

         A156: 1 <= (m + 1) by NAT_1: 12;

        

         A157: (m + 1) <= ((( len c) + 1) + 1) by A23, XREAL_1: 6;

        

         A158: (( len p2) + m) = ((( len c) + 1) + 1) by A22, A23, A24, FINSEQ_6:def 4

        .= (( len p29) + (m + 1)) by A24, A156, A157, Lm2

        .= ((( len p29) + 1) + m);

        

         A159: ( len ( Sgm DR)) = ( card DR) by A141, FINSEQ_3: 39;

        DL = ( Seg n) by FINSEQ_1:def 1;

        then

         A160: ( Sgm DL) = ( idseq n) by FINSEQ_3: 48;

        then

         A161: ( dom ( Sgm DL)) = ( Seg n);

        ( rng ( Sgm DL)) = DL by A141, FINSEQ_1:def 13;

        then

         A162: ( rng ( Sgm DL)) c= ( dom fvs) by A50, A140, XBOOLE_1: 7;

        ( rng ( Sgm DR)) = DR by A141, FINSEQ_1:def 13;

        then

         A163: ( rng ( Sgm DR)) c= ( dom fvs) by A50, A140, XBOOLE_1: 7;

        set SL = ( Sgm DL);

        set SR = ( Sgm DR);

        now

          let p be object;

          hereby

            assume

             A164: p in pp;

            then

            consider x,y be object such that

             A165: p = [x, y] by RELAT_1:def 1;

            

             A166: x in ( dom pp) by A164, A165, FUNCT_1: 1;

            

             A167: y = (pp . x) by A164, A165, FUNCT_1: 1;

            reconsider k = x as Element of NAT by A166;

            

             A168: 1 <= k by A166, FINSEQ_3: 25;

            

             A169: k <= ( len pp) by A166, FINSEQ_3: 25;

            then

             A170: x in ( dom SL) by A11, A27, A66, A161, A168, FINSEQ_1: 1;

            then

             A171: k = (SL . k) by A160, FUNCT_1: 18;

            

             A172: k in domfvs by A11, A27, A66, A168, A169;

            then

             A173: x in ( dom (fvs * SL)) by A50, A170, A171, FUNCT_1: 11;

            ( 0 + 1) <= k by A166, FINSEQ_3: 25;

            then

            consider i be Nat such that 0 <= i and

             A174: i < n and

             A175: k = (i + 1) by A11, A27, A66, A169, FINSEQ_6: 127;

            ((fvs * SL) . x) = (fvs . k) by A171, A173, FUNCT_1: 12

            .= (vs . (1 + i)) by A50, A172, A175, GRFUNC_1: 2

            .= y by A3, A11, A21, A27, A66, A167, A174, A175, FINSEQ_6:def 4;

            hence p in (fvs * ( Sgm DL)) by A165, A173, FUNCT_1: 1;

          end;

          assume

           A176: p in (fvs * ( Sgm DL));

          then

          consider x,y be object such that

           A177: p = [x, y] by RELAT_1:def 1;

          

           A178: x in ( dom (fvs * SL)) by A176, A177, FUNCT_1: 1;

          

           A179: y = ((fvs * SL) . x) by A176, A177, FUNCT_1: 1;

          

           A180: ((fvs * SL) . x) = (fvs . (SL . x)) by A178, FUNCT_1: 12;

          

           A181: x in ( dom SL) by A178, FUNCT_1: 11;

          then x in { kk where kk be Nat : 1 <= kk & kk <= n } by A161, FINSEQ_1:def 1;

          then

          consider k be Nat such that

           A182: k = x and

           A183: 1 <= k and

           A184: k <= n;

          

           A185: k in ( dom fvs) by A50, A183, A184;

          

           A186: k = (SL . k) by A160, A181, A182, FUNCT_1: 18;

          

           A187: k in ( dom pp) by A11, A27, A66, A183, A184, FINSEQ_3: 25;

          ( 0 + 1) <= k by A183;

          then ex i be Nat st ( 0 <= i) & (i < n) & (k = (i + 1)) by A184, FINSEQ_6: 127;

          

          then (pp . k) = (vs . k) by A3, A11, A21, A27, A66, FINSEQ_6:def 4

          .= y by A179, A180, A182, A185, A186, GRFUNC_1: 2;

          hence p in pp by A177, A182, A187, FUNCT_1: 1;

        end;

        then

         A188: pp = (fvs * ( Sgm DL)) by TARSKI: 2;

        

         A189: ((m + 1) + lp22) = (m + lp21);

        

         A190: 1 <= (m + 1) by NAT_1: 12;

        

         A191: (m + 1) <= ((( len c) + 1) + 1) by A5, A8, XREAL_1: 7;

        now

          let p be object;

          hereby

            assume

             A192: p in p29;

            then

            consider x,y be object such that

             A193: p = [x, y] by RELAT_1:def 1;

            

             A194: x in ( dom p29) by A192, A193, FUNCT_1: 1;

            

             A195: y = (p29 . x) by A192, A193, FUNCT_1: 1;

            reconsider k = x as Element of NAT by A194;

            

             A196: 1 <= k by A194, FINSEQ_3: 25;

            

             A197: k <= ( len p29) by A194, FINSEQ_3: 25;

            

             A198: x in ( dom SR) by A155, A158, A159, A194, FINSEQ_3: 29;

            

             A199: (m + k) = (SR . k) by A8, A154, A158, A189, A196, A197, FINSEQ_6: 131;

            

             A200: (SR . k) in ( rng SR) by A198, FUNCT_1:def 3;

            then

             A201: x in ( dom (fvs * SR)) by A163, A198, FUNCT_1: 11;

            ( 0 + 1) <= k by A194, FINSEQ_3: 25;

            then

            consider i be Nat such that 0 <= i and

             A202: i < ( len p29) and

             A203: k = (i + 1) by A197, FINSEQ_6: 127;

            ((fvs * SR) . x) = (fvs . (m + k)) by A199, A201, FUNCT_1: 12

            .= (vs . ((m + 1) + i)) by A163, A199, A200, A203, GRFUNC_1: 2

            .= y by A8, A190, A191, A195, A202, A203, Lm2;

            hence p in (fvs * ( Sgm DR)) by A193, A201, FUNCT_1: 1;

          end;

          assume

           A204: p in (fvs * ( Sgm DR));

          then

          consider x,y be object such that

           A205: p = [x, y] by RELAT_1:def 1;

          

           A206: x in ( dom (fvs * SR)) by A204, A205, FUNCT_1: 1;

          

           A207: y = ((fvs * SR) . x) by A204, A205, FUNCT_1: 1;

          

           A208: x in ( dom SR) by A206, FUNCT_1: 11;

          

           A209: (SR . x) in ( dom fvs) by A206, FUNCT_1: 11;

          reconsider k = x as Element of NAT by A208;

          

           A210: k in ( dom p29) by A155, A158, A159, A208, FINSEQ_3: 29;

          

           A211: 1 <= k by A208, FINSEQ_3: 25;

          

           A212: k <= ( len p29) by A155, A158, A159, A208, FINSEQ_3: 25;

          then

           A213: (m + k) = (SR . k) by A8, A154, A158, A189, A211, FINSEQ_6: 131;

          ( 0 + 1) <= k by A208, FINSEQ_3: 25;

          then

          consider i be Nat such that 0 <= i and

           A214: i < ( len p29) and

           A215: k = (i + 1) by A212, FINSEQ_6: 127;

          (p29 . k) = (vs . ((m + 1) + i)) by A8, A190, A191, A214, A215, Lm2

          .= (fvs . (SR . k)) by A209, A213, A215, GRFUNC_1: 2

          .= y by A207, A208, FUNCT_1: 13;

          hence p in p29 by A205, A210, FUNCT_1: 1;

        end;

        then

         A216: p29 = (fvs * ( Sgm DR)) by TARSKI: 2;

        ( Seq fvs) = (fvs * (( Sgm DL) ^ ( Sgm DR))) by A50, A140, A153, FINSEQ_1:def 14;

        hence thesis by A65, A162, A163, A188, A216, FINSEQ_6: 150;

      end;

        suppose

         A217: n = 1 & m <> ( len vs);

        then

         A218: m < ( len vs) by A5, XXREAL_0: 1;

        then

         A219: m <= ( len c) by A8, NAT_1: 13;

        

         A220: 1 < m by A3, A4, XXREAL_0: 2;

        

         A221: 1 <= m by A3, A4, XXREAL_0: 2;

        

         A222: m <= ( len c) by A8, A218, NAT_1: 13;

        reconsider c2 = ((m,( len c)) -cut c) as oriented Chain of G by A219, A220, Th12;

        set p2 = ((m,(( len c) + 1)) -cut vs);

        

         A223: p2 is_oriented_vertex_seq_of c2 by A2, A219, A220, Th13;

        set domfc = { k where k be Nat : m <= k & k <= ( len c) };

        deffunc F( object) = (c . $1);

        consider fc be Function such that

         A224: ( dom fc) = domfc and

         A225: for x be object st x in domfc holds (fc . x) = F(x) from FUNCT_1:sch 3;

        domfc c= ( Seg ( len c))

        proof

          let x be object;

          assume x in domfc;

          then

          consider kk be Nat such that

           A226: x = kk and

           A227: m <= kk and

           A228: kk <= ( len c);

          1 <= kk by A220, A227, XXREAL_0: 2;

          hence thesis by A226, A228, FINSEQ_1: 1;

        end;

        then

        reconsider fc as FinSubsequence by A224, FINSEQ_1:def 12;

        fc c= c

        proof

          let p be object;

          assume

           A229: p in fc;

          then

          consider x,y be object such that

           A230: [x, y] = p by RELAT_1:def 1;

          

           A231: x in ( dom fc) by A229, A230, FUNCT_1: 1;

          

           A232: y = (fc . x) by A229, A230, FUNCT_1: 1;

          consider kk be Nat such that

           A233: x = kk and

           A234: m <= kk and

           A235: kk <= ( len c) by A224, A231;

          1 <= kk by A220, A234, XXREAL_0: 2;

          then

           A236: x in ( dom c) by A233, A235, FINSEQ_3: 25;

          y = (c . kk) by A224, A225, A231, A232, A233;

          hence thesis by A230, A233, A236, FUNCT_1: 1;

        end;

        then

        reconsider fc as Subset of c;

        take fc;

        set domfvs = { k where k be Nat : m <= k & k <= ( len vs) };

        deffunc F( object) = (vs . $1);

        consider fvs be Function such that

         A237: ( dom fvs) = domfvs and

         A238: for x be object st x in domfvs holds (fvs . x) = F(x) from FUNCT_1:sch 3;

        domfvs c= ( Seg ( len vs))

        proof

          let x be object;

          assume x in domfvs;

          then

          consider kk be Nat such that

           A239: x = kk and

           A240: m <= kk and

           A241: kk <= ( len vs);

          1 <= kk by A220, A240, XXREAL_0: 2;

          hence thesis by A239, A241, FINSEQ_1: 1;

        end;

        then

        reconsider fvs as FinSubsequence by A237, FINSEQ_1:def 12;

        fvs c= vs

        proof

          let p be object;

          assume

           A242: p in fvs;

          then

          consider x,y be object such that

           A243: [x, y] = p by RELAT_1:def 1;

          

           A244: x in ( dom fvs) by A242, A243, FUNCT_1: 1;

          

           A245: y = (fvs . x) by A242, A243, FUNCT_1: 1;

          consider kk be Nat such that

           A246: x = kk and

           A247: m <= kk and

           A248: kk <= ( len vs) by A237, A244;

          1 <= kk by A220, A247, XXREAL_0: 2;

          then

           A249: x in ( dom vs) by A246, A248, FINSEQ_3: 25;

          y = (vs . kk) by A237, A238, A244, A245, A246;

          hence thesis by A243, A246, A249, FUNCT_1: 1;

        end;

        then

        reconsider fvs as Subset of vs;

        take fvs;

        take c1 = c2;

        take p1 = p2;

        

         A250: (( len c2) + m) = (( len c) + 1) by A4, A5, A8, A217, Lm2;

        

         A251: (m - m) <= (( len c) - m) by A219, XREAL_1: 9;

        (1 - 1) <= (m - 1) by A220, XREAL_1: 9;

        then (m -' 1) = (m - 1) by XREAL_0:def 2;

        then

        reconsider m1 = (m - 1) as Element of NAT ;

        

         A252: m = (m1 + 1);

        (( len c2) -' 1) = (( len c2) - 1) by A250, A251, XREAL_0:def 2;

        then

        reconsider lc21 = (( len c2) - 1) as Element of NAT ;

        

         A253: (m + lc21) = (m1 + ( len c2));

        

         A254: m <= ((( len c) + 1) + 1) by A5, A8, NAT_1: 12;

        

         A255: (( len c) + 1) <= ( len vs) by A2;

        then

         A256: (( len p2) + m) = ((( len c) + 1) + 1) by A4, A217, A254, Lm2;

        then ( len p2) = (((( len c) - m) + 1) + 1);

        then

         A257: 1 <= ( len p2) by A250, NAT_1: 12;

        

         A258: ( len c2) = (( len c) + (( - m) + 1)) by A250;

        (1 - 1) < (m - 1) by A220, XREAL_1: 9;

        then 0 < ( - ( - (m - 1)));

        then ( - (m - 1)) < 0 ;

        hence

         A259: ( len c1) < ( len c) by A258, XREAL_1: 30;

        thus p1 is_oriented_vertex_seq_of c1 by A2, A221, A222, Th13;

        ( len p1) = (( len c1) + 1) by A223;

        hence ( len p1) < ( len vs) by A8, A259, XREAL_1: 6;

        thus (vs . 1) = (p1 . 1) by A4, A5, A6, A8, A217, FINSEQ_6: 138;

        thus (vs . ( len vs)) = (p1 . ( len p1)) by A4, A5, A8, A217, FINSEQ_6: 138;

        

         A260: domfc c= ( Seg ( len c))

        proof

          let x be object;

          assume x in domfc;

          then

          consider k be Nat such that

           A261: x = k and

           A262: m <= k and

           A263: k <= ( len c);

          1 <= k by A220, A262, XXREAL_0: 2;

          hence thesis by A261, A263, FINSEQ_1: 1;

        end;

        then

        reconsider domfc as finite set by FINSET_1: 1;

        (( len c2) -' 1) = (( len c2) - 1) by A250, A251, XREAL_0:def 2;

        then

        reconsider lc21 = (( len c2) - 1) as Element of NAT ;

        (m + lc21) = ( len c) by A250;

        

        then

         A264: ( card domfc) = ((( len c2) + ( - 1)) + 1) by FINSEQ_6: 130

        .= ( len c2);

        

         A265: ( len ( Sgm domfc)) = ( card domfc) by A260, FINSEQ_3: 39;

        

         A266: ( rng ( Sgm domfc)) c= ( dom fc) by A224, A260, FINSEQ_1:def 13;

        set SR = ( Sgm domfc);

        now

          let p be object;

          hereby

            assume

             A267: p in c2;

            then

            consider x,y be object such that

             A268: p = [x, y] by RELAT_1:def 1;

            

             A269: x in ( dom c2) by A267, A268, FUNCT_1: 1;

            

             A270: y = (c2 . x) by A267, A268, FUNCT_1: 1;

            reconsider k = x as Element of NAT by A269;

            

             A271: 1 <= k by A269, FINSEQ_3: 25;

            

             A272: k <= ( len c2) by A269, FINSEQ_3: 25;

            

             A273: x in ( dom SR) by A264, A265, A269, FINSEQ_3: 29;

            

             A274: (m1 + k) = (SR . k) by A250, A252, A253, A271, A272, FINSEQ_6: 131;

            

             A275: (SR . k) in ( rng SR) by A273, FUNCT_1:def 3;

            then

             A276: x in ( dom (fc * SR)) by A266, A273, FUNCT_1: 11;

            ( 0 + 1) <= k by A269, FINSEQ_3: 25;

            then

            consider i be Nat such that 0 <= i and

             A277: i < ( len c2) and

             A278: k = (i + 1) by A272, FINSEQ_6: 127;

            ((fc * SR) . x) = (fc . (m1 + k)) by A274, A276, FUNCT_1: 12

            .= (c . (m + i)) by A266, A274, A275, A278, GRFUNC_1: 2

            .= y by A4, A5, A8, A217, A270, A277, A278, Lm2;

            hence p in (fc * ( Sgm domfc)) by A268, A276, FUNCT_1: 1;

          end;

          assume

           A279: p in (fc * ( Sgm domfc));

          then

          consider x,y be object such that

           A280: p = [x, y] by RELAT_1:def 1;

          

           A281: x in ( dom (fc * SR)) by A279, A280, FUNCT_1: 1;

          

           A282: y = ((fc * SR) . x) by A279, A280, FUNCT_1: 1;

          

           A283: x in ( dom SR) by A281, FUNCT_1: 11;

          

           A284: (SR . x) in ( dom fc) by A281, FUNCT_1: 11;

          reconsider k = x as Element of NAT by A283;

          

           A285: k in ( dom c2) by A264, A265, A283, FINSEQ_3: 29;

          

           A286: 1 <= k by A283, FINSEQ_3: 25;

          

           A287: k <= ( len c2) by A264, A265, A283, FINSEQ_3: 25;

          then

           A288: (m1 + k) = (SR . k) by A250, A252, A253, A286, FINSEQ_6: 131;

          ( 0 + 1) <= k by A283, FINSEQ_3: 25;

          then

          consider i be Nat such that 0 <= i and

           A289: i < ( len c2) and

           A290: k = (i + 1) by A287, FINSEQ_6: 127;

          (c2 . k) = (c . ((m1 + 1) + i)) by A4, A5, A8, A217, A289, A290, Lm2

          .= (fc . (SR . k)) by A284, A288, A290, GRFUNC_1: 2

          .= y by A282, A283, FUNCT_1: 13;

          hence p in c2 by A280, A285, FUNCT_1: 1;

        end;

        then c2 = (fc * ( Sgm domfc)) by TARSKI: 2;

        hence ( Seq fc) = c1 by A224, FINSEQ_1:def 14;

        

         A291: domfvs c= ( Seg ( len vs))

        proof

          let x be object;

          assume x in domfvs;

          then

          consider k be Nat such that

           A292: x = k and

           A293: m <= k and

           A294: k <= ( len vs);

          1 <= k by A220, A293, XXREAL_0: 2;

          hence thesis by A292, A294, FINSEQ_1: 1;

        end;

        then

        reconsider domfvs as finite set by FINSET_1: 1;

        (1 - 1) <= (( len p2) - 1) by A257, XREAL_1: 9;

        then (( len p2) -' 1) = (( len p2) - 1) by XREAL_0:def 2;

        then

        reconsider lp21 = (( len p2) - 1) as Element of NAT ;

        

         A295: (m + lp21) = (( len c) + 1) by A256;

        

         A296: (m + lp21) = (m1 + ( len p2));

        

         A297: ( card domfvs) = ((( len p2) + ( - 1)) + 1) by A8, A295, FINSEQ_6: 130

        .= ( len p2);

        

         A298: ( len ( Sgm domfvs)) = ( card domfvs) by A291, FINSEQ_3: 39;

        

         A299: ( rng ( Sgm domfvs)) c= ( dom fvs) by A237, A291, FINSEQ_1:def 13;

        set SR = ( Sgm domfvs);

        now

          let p be object;

          hereby

            assume

             A300: p in p2;

            then

            consider x,y be object such that

             A301: p = [x, y] by RELAT_1:def 1;

            

             A302: x in ( dom p2) by A300, A301, FUNCT_1: 1;

            

             A303: y = (p2 . x) by A300, A301, FUNCT_1: 1;

            reconsider k = x as Element of NAT by A302;

            

             A304: 1 <= k by A302, FINSEQ_3: 25;

            

             A305: k <= ( len p2) by A302, FINSEQ_3: 25;

            

             A306: x in ( dom SR) by A297, A298, A302, FINSEQ_3: 29;

            

             A307: (m1 + k) = (SR . k) by A8, A252, A256, A296, A304, A305, FINSEQ_6: 131;

            

             A308: (SR . k) in ( rng SR) by A306, FUNCT_1:def 3;

            then

             A309: x in ( dom (fvs * SR)) by A299, A306, FUNCT_1: 11;

            ( 0 + 1) <= k by A302, FINSEQ_3: 25;

            then

            consider i be Nat such that 0 <= i and

             A310: i < ( len p2) and

             A311: k = (i + 1) by A305, FINSEQ_6: 127;

            ((fvs * SR) . x) = (fvs . (m1 + k)) by A307, A309, FUNCT_1: 12

            .= (vs . (m + i)) by A299, A307, A308, A311, GRFUNC_1: 2

            .= y by A4, A217, A254, A255, A303, A310, A311, Lm2;

            hence p in (fvs * ( Sgm domfvs)) by A301, A309, FUNCT_1: 1;

          end;

          assume

           A312: p in (fvs * ( Sgm domfvs));

          then

          consider x,y be object such that

           A313: p = [x, y] by RELAT_1:def 1;

          

           A314: x in ( dom (fvs * SR)) by A312, A313, FUNCT_1: 1;

          

           A315: y = ((fvs * SR) . x) by A312, A313, FUNCT_1: 1;

          

           A316: x in ( dom SR) by A314, FUNCT_1: 11;

          

           A317: (SR . x) in ( dom fvs) by A314, FUNCT_1: 11;

          reconsider k = x as Element of NAT by A316;

          

           A318: k in ( dom p2) by A297, A298, A316, FINSEQ_3: 29;

          

           A319: 1 <= k by A316, FINSEQ_3: 25;

          

           A320: k <= ( len p2) by A297, A298, A316, FINSEQ_3: 25;

          then

           A321: (m1 + k) = (SR . k) by A8, A252, A256, A296, A319, FINSEQ_6: 131;

          ( 0 + 1) <= k by A316, FINSEQ_3: 25;

          then

          consider i be Nat such that 0 <= i and

           A322: i < ( len p2) and

           A323: k = (i + 1) by A320, FINSEQ_6: 127;

          (p2 . k) = (vs . ((m1 + 1) + i)) by A4, A217, A254, A255, A322, A323, Lm2

          .= (fvs . (SR . k)) by A317, A321, A323, GRFUNC_1: 2

          .= y by A315, A316, FUNCT_1: 13;

          hence p in p2 by A313, A318, FUNCT_1: 1;

        end;

        then p2 = (fvs * ( Sgm domfvs)) by TARSKI: 2;

        hence thesis by A237, FINSEQ_1:def 14;

      end;

        suppose

         A324: n <> 1 & m = ( len vs);

        then 1 < n by A3, XXREAL_0: 1;

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

        then

         A325: ((1 + 1) - 1) <= (n - 1) by XREAL_1: 9;

        n < ( len vs) by A4, A5, XXREAL_0: 2;

        then

         A326: (n - 1) < ((( len c) + 1) - 1) by A8, XREAL_1: 9;

        

         A327: 1 <= (n1 + 1) by NAT_1: 12;

        reconsider c1 = ((1,n1) -cut c) as oriented Chain of G by A11, A325, A326, Th12;

        set pp = ((1,n) -cut vs);

        

         A328: n <= ( len vs) by A4, A5, XXREAL_0: 2;

        

         A329: pp is_oriented_vertex_seq_of c1 by A2, A12, A325, A326, Th13;

        then

         A330: ( len pp) = (( len c1) + 1);

        set domfc = { k where k be Nat : 1 <= k & k <= n1 };

        deffunc F( object) = (c . $1);

        consider fc be Function such that

         A331: ( dom fc) = domfc and

         A332: for x be object st x in domfc holds (fc . x) = F(x) from FUNCT_1:sch 3;

        domfc c= ( Seg ( len c))

        proof

          let x be object;

          assume x in domfc;

          then

          consider kk be Nat such that

           A333: x = kk and

           A334: 1 <= kk and

           A335: kk <= n1;

          kk <= ( len c) by A11, A326, A335, XXREAL_0: 2;

          hence thesis by A333, A334, FINSEQ_1: 1;

        end;

        then

        reconsider fc as FinSubsequence by A331, FINSEQ_1:def 12;

        fc c= c

        proof

          let p be object;

          assume

           A336: p in fc;

          then

          consider x,y be object such that

           A337: [x, y] = p by RELAT_1:def 1;

          

           A338: x in ( dom fc) by A336, A337, FUNCT_1: 1;

          

           A339: y = (fc . x) by A336, A337, FUNCT_1: 1;

          consider kk be Nat such that

           A340: x = kk and

           A341: 1 <= kk and

           A342: kk <= n1 by A331, A338;

          kk <= ( len c) by A11, A326, A342, XXREAL_0: 2;

          then

           A343: x in ( dom c) by A340, A341, FINSEQ_3: 25;

          y = (c . kk) by A331, A332, A338, A339, A340;

          hence thesis by A337, A340, A343, FUNCT_1: 1;

        end;

        then

        reconsider fc as Subset of c;

        take fc;

        set domfvs = { k where k be Nat : 1 <= k & k <= n };

        deffunc F( object) = (vs . $1);

        consider fvs be Function such that

         A344: ( dom fvs) = domfvs and

         A345: for x be object st x in domfvs holds (fvs . x) = F(x) from FUNCT_1:sch 3;

        domfvs c= ( Seg ( len vs))

        proof

          let x be object;

          assume x in domfvs;

          then

          consider kk be Nat such that

           A346: x = kk and

           A347: 1 <= kk and

           A348: kk <= n;

          kk <= ( len vs) by A328, A348, XXREAL_0: 2;

          hence thesis by A346, A347, FINSEQ_1: 1;

        end;

        then

        reconsider fvs as FinSubsequence by A344, FINSEQ_1:def 12;

        fvs c= vs

        proof

          let p be object;

          assume

           A349: p in fvs;

          then

          consider x,y be object such that

           A350: [x, y] = p by RELAT_1:def 1;

          

           A351: x in ( dom fvs) by A349, A350, FUNCT_1: 1;

          

           A352: y = (fvs . x) by A349, A350, FUNCT_1: 1;

          consider kk be Nat such that

           A353: x = kk and

           A354: 1 <= kk and

           A355: kk <= n by A344, A351;

          kk <= ( len vs) by A328, A355, XXREAL_0: 2;

          then

           A356: x in ( dom vs) by A353, A354, FINSEQ_3: 25;

          y = (vs . kk) by A344, A345, A351, A352, A353;

          hence thesis by A350, A353, A356, FUNCT_1: 1;

        end;

        then

        reconsider fvs as Subset of vs;

        take fvs;

        take c9 = c1;

        take p1 = pp;

        

         A357: (( len c1) + 1) = (n1 + 1) by A11, A326, A327, Lm2;

        then

         A358: ( len c1) = (n - 1) by A10, XREAL_0:def 2;

        thus ( len c9) < ( len c) by A10, A326, A357, XREAL_0:def 2;

        thus p1 is_oriented_vertex_seq_of c9 by A2, A12, A325, A326, Th13;

        ( len p1) = (( len c1) + 1) by A329;

        hence ( len p1) < ( len vs) by A4, A5, A358, XXREAL_0: 2;

        thus (vs . 1) = (p1 . 1) by A3, A328, FINSEQ_6: 138;

        thus (vs . ( len vs)) = (p1 . ( len p1)) by A3, A4, A6, A324, FINSEQ_6: 138;

        domfc c= ( Seg ( len c))

        proof

          let x be object;

          assume x in domfc;

          then

          consider k be Nat such that

           A359: x = k and

           A360: 1 <= k and

           A361: k <= n1;

          k <= ( len c) by A11, A326, A361, XXREAL_0: 2;

          hence thesis by A359, A360, FINSEQ_1: 1;

        end;

        then

        reconsider domfc as finite set by FINSET_1: 1;

        domfc = ( Seg n1) by FINSEQ_1:def 1;

        then

         A362: ( Sgm domfc) = ( idseq n1) by FINSEQ_3: 48;

        then

         A363: ( dom ( Sgm domfc)) = ( Seg n1);

        set SL = ( Sgm domfc);

        now

          let p be object;

          hereby

            assume

             A364: p in c1;

            then

            consider x,y be object such that

             A365: p = [x, y] by RELAT_1:def 1;

            

             A366: x in ( dom c1) by A364, A365, FUNCT_1: 1;

            

             A367: y = (c1 . x) by A364, A365, FUNCT_1: 1;

            reconsider k = x as Element of NAT by A366;

            

             A368: 1 <= k by A366, FINSEQ_3: 25;

            

             A369: k <= ( len c1) by A366, FINSEQ_3: 25;

            then

             A370: x in ( dom SL) by A357, A363, A368, FINSEQ_1: 1;

            then

             A371: k = (SL . k) by A362, FUNCT_1: 18;

            

             A372: k in domfc by A357, A368, A369;

            then

             A373: x in ( dom (fc * SL)) by A331, A370, A371, FUNCT_1: 11;

            ( 0 + 1) <= k by A366, FINSEQ_3: 25;

            then

            consider i be Nat such that 0 <= i and

             A374: i < n1 and

             A375: k = (i + 1) by A357, A369, FINSEQ_6: 127;

            ((fc * SL) . x) = (fc . k) by A371, A373, FUNCT_1: 12

            .= (c . (1 + i)) by A331, A372, A375, GRFUNC_1: 2

            .= y by A11, A326, A327, A357, A367, A374, A375, Lm2;

            hence p in (fc * ( Sgm domfc)) by A365, A373, FUNCT_1: 1;

          end;

          assume

           A376: p in (fc * ( Sgm domfc));

          then

          consider x,y be object such that

           A377: p = [x, y] by RELAT_1:def 1;

          

           A378: x in ( dom (fc * SL)) by A376, A377, FUNCT_1: 1;

          

           A379: y = ((fc * SL) . x) by A376, A377, FUNCT_1: 1;

          

           A380: ((fc * SL) . x) = (fc . (SL . x)) by A378, FUNCT_1: 12;

          

           A381: x in ( dom SL) by A378, FUNCT_1: 11;

          then x in { kk where kk be Nat : 1 <= kk & kk <= n1 } by A363, FINSEQ_1:def 1;

          then

          consider k be Nat such that

           A382: k = x and

           A383: 1 <= k and

           A384: k <= n1;

          

           A385: k in ( dom fc) by A331, A383, A384;

          

           A386: k = (SL . k) by A362, A381, A382, FUNCT_1: 18;

          

           A387: k in ( dom c1) by A357, A383, A384, FINSEQ_3: 25;

          ( 0 + 1) <= k by A383;

          then ex i be Nat st ( 0 <= i) & (i < n1) & (k = (i + 1)) by A384, FINSEQ_6: 127;

          

          then (c1 . k) = (c . k) by A11, A326, A327, A357, Lm2

          .= y by A379, A380, A382, A385, A386, GRFUNC_1: 2;

          hence p in c1 by A377, A382, A387, FUNCT_1: 1;

        end;

        then c1 = (fc * ( Sgm domfc)) by TARSKI: 2;

        hence ( Seq fc) = c9 by A331, FINSEQ_1:def 14;

        domfvs c= ( Seg ( len vs))

        proof

          let x be object;

          assume x in domfvs;

          then

          consider k be Nat such that

           A388: x = k and

           A389: 1 <= k and

           A390: k <= n;

          k <= ( len vs) by A328, A390, XXREAL_0: 2;

          hence thesis by A388, A389, FINSEQ_1: 1;

        end;

        then

        reconsider domfvs as finite set by FINSET_1: 1;

        domfvs = ( Seg n) by FINSEQ_1:def 1;

        then

         A391: ( Sgm domfvs) = ( idseq n) by FINSEQ_3: 48;

        then

         A392: ( dom ( Sgm domfvs)) = ( Seg n);

        set SL = ( Sgm domfvs);

        now

          let p be object;

          hereby

            assume

             A393: p in pp;

            then

            consider x,y be object such that

             A394: p = [x, y] by RELAT_1:def 1;

            

             A395: x in ( dom pp) by A393, A394, FUNCT_1: 1;

            

             A396: y = (pp . x) by A393, A394, FUNCT_1: 1;

            reconsider k = x as Element of NAT by A395;

            

             A397: 1 <= k by A395, FINSEQ_3: 25;

            

             A398: k <= ( len pp) by A395, FINSEQ_3: 25;

            then

             A399: x in ( dom SL) by A330, A358, A392, A397, FINSEQ_1: 1;

            then

             A400: k = (SL . k) by A391, FUNCT_1: 18;

            

             A401: k in domfvs by A330, A358, A397, A398;

            then

             A402: x in ( dom (fvs * SL)) by A344, A399, A400, FUNCT_1: 11;

            ( 0 + 1) <= k by A395, FINSEQ_3: 25;

            then

            consider i be Nat such that 0 <= i and

             A403: i < n and

             A404: k = (i + 1) by A330, A358, A398, FINSEQ_6: 127;

            ((fvs * SL) . x) = (fvs . k) by A400, A402, FUNCT_1: 12

            .= (vs . (1 + i)) by A344, A401, A404, GRFUNC_1: 2

            .= y by A3, A328, A330, A358, A396, A403, A404, FINSEQ_6:def 4;

            hence p in (fvs * ( Sgm domfvs)) by A394, A402, FUNCT_1: 1;

          end;

          assume

           A405: p in (fvs * ( Sgm domfvs));

          then

          consider x,y be object such that

           A406: p = [x, y] by RELAT_1:def 1;

          

           A407: x in ( dom (fvs * SL)) by A405, A406, FUNCT_1: 1;

          

           A408: y = ((fvs * SL) . x) by A405, A406, FUNCT_1: 1;

          

           A409: ((fvs * SL) . x) = (fvs . (SL . x)) by A407, FUNCT_1: 12;

          

           A410: x in ( dom SL) by A407, FUNCT_1: 11;

          then x in { kk where kk be Nat : 1 <= kk & kk <= n } by A392, FINSEQ_1:def 1;

          then

          consider k be Nat such that

           A411: k = x and

           A412: 1 <= k and

           A413: k <= n;

          

           A414: k in ( dom fvs) by A344, A412, A413;

          

           A415: k = (SL . k) by A391, A410, A411, FUNCT_1: 18;

          

           A416: k in ( dom pp) by A330, A358, A412, A413, FINSEQ_3: 25;

          ( 0 + 1) <= k by A412;

          then ex i be Nat st ( 0 <= i) & (i < n) & (k = (i + 1)) by A413, FINSEQ_6: 127;

          

          then (pp . k) = (vs . k) by A3, A328, A330, A358, FINSEQ_6:def 4

          .= y by A408, A409, A411, A414, A415, GRFUNC_1: 2;

          hence p in pp by A406, A411, A416, FUNCT_1: 1;

        end;

        then pp = (fvs * ( Sgm domfvs)) by TARSKI: 2;

        hence thesis by A344, FINSEQ_1:def 14;

      end;

    end;

    theorem :: GRAPH_4:21

    vs is_oriented_vertex_seq_of c implies ex fc be Subset of c, fvs be Subset of vs, sc, vs1 st ( Seq fc) = sc & ( Seq fvs) = vs1 & vs1 is_oriented_vertex_seq_of sc & (vs . 1) = (vs1 . 1) & (vs . ( len vs)) = (vs1 . ( len vs1))

    proof

      assume

       A1: vs is_oriented_vertex_seq_of c;

      per cases ;

        suppose

         A2: c is Simple;

        reconsider fc = c as Subset of c by FINSEQ_6: 152;

        reconsider fvs = vs as Subset of vs by FINSEQ_6: 152;

        reconsider sc = c as oriented simple Chain of G by A2, Th19;

        take fc, fvs, sc, vs;

        thus ( Seq fc) = sc & ( Seq fvs) = vs by FINSEQ_3: 116;

        thus vs is_oriented_vertex_seq_of sc by A1;

        thus thesis;

      end;

        suppose

         A3: not c is Simple;

        defpred P[ Nat] means ex fc be Subset of c, fvs be Subset of vs, c1, vs1 st ( Seq fc) = c1 & ( Seq fvs) = vs1 & vs1 is_oriented_vertex_seq_of c1 & (vs . 1) = (vs1 . 1) & (vs . ( len vs)) = (vs1 . ( len vs1)) & ( len c1) = $1 & not c1 is Simple;

         P[( len c)]

        proof

          reconsider fc = c as Subset of c by FINSEQ_6: 152;

          reconsider fvs = vs as Subset of vs by FINSEQ_6: 152;

          take fc, fvs, c, vs;

          thus ( Seq fc) = c & ( Seq fvs) = vs by FINSEQ_3: 116;

          thus vs is_oriented_vertex_seq_of c by A1;

          thus (vs . 1) = (vs . 1) & (vs . ( len vs)) = (vs . ( len vs));

          thus thesis by A3;

        end;

        then

         A4: ex k be Nat st P[k];

        consider k be Nat such that

         A5: P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A4);

        consider fc be Subset of c, fvs be Subset of vs, c1, vs1 such that

         A6: ( Seq fc) = c1 and

         A7: ( Seq fvs) = vs1 and

         A8: vs1 is_oriented_vertex_seq_of c1 and

         A9: (vs . 1) = (vs1 . 1) and

         A10: (vs . ( len vs)) = (vs1 . ( len vs1)) and

         A11: ( len c1) = k and

         A12: not c1 is Simple by A5;

        consider fc1 be Subset of c1, fvs1 be Subset of vs1, c2, vs2 such that

         A13: ( len c2) < ( len c1) and

         A14: vs2 is_oriented_vertex_seq_of c2 and ( len vs2) < ( len vs1) and

         A15: (vs1 . 1) = (vs2 . 1) and

         A16: (vs1 . ( len vs1)) = (vs2 . ( len vs2)) and

         A17: ( Seq fc1) = c2 and

         A18: ( Seq fvs1) = vs2 by A8, A12, Th20;

        reconsider fc9 = (fc | ( rng (( Sgm ( dom fc)) | ( dom fc1)))) as Subset of c by FINSEQ_6: 153;

        

         A19: ( Seq fc9) = c2 by A6, A17, FINSEQ_6: 154;

        reconsider fvs9 = (fvs | ( rng (( Sgm ( dom fvs)) | ( dom fvs1)))) as Subset of vs by FINSEQ_6: 153;

        

         A20: ( Seq fvs9) = vs2 by A7, A18, FINSEQ_6: 154;

        now

          assume c2 is Simple oriented Chain of G;

          then

          reconsider sc = c2 as oriented simple Chain of G by Th19;

          take fc9, sc;

          ( Seq fc9) = sc by A6, A17, FINSEQ_6: 154;

          hence thesis by A9, A10, A14, A15, A16, A20;

        end;

        hence thesis by A5, A9, A10, A11, A13, A14, A15, A16, A19, A20;

      end;

    end;

    theorem :: GRAPH_4:22

    p is OrientedPath of G implies (p | ( Seg n)) is OrientedPath of G

    proof

      assume

       A1: p is OrientedPath of G;

      then

      reconsider p9 = (p | ( Seg n)) as oriented Chain of G by Th16;

      reconsider q = (p | ( Seg n)) as FinSequence;

      now

        let n1,m1 be Nat;

        assume that

         A2: 1 <= n1 and

         A3: n1 < m1 and

         A4: m1 <= ( len q);

        1 < m1 by A2, A3, XXREAL_0: 2;

        then m1 in ( dom q) by A4, FINSEQ_3: 25;

        then

         A5: (q . m1) = (p . m1) by FUNCT_1: 47;

        n1 < ( len q) by A3, A4, XXREAL_0: 2;

        then n1 in ( dom q) by A2, FINSEQ_3: 25;

        then

         A6: (q . n1) = (p . n1) by FUNCT_1: 47;

        ( dom q) c= ( dom p) by RELAT_1: 60;

        then ( dom q) c= ( Seg ( len p)) by FINSEQ_1:def 3;

        then ( Seg ( len q)) c= ( Seg ( len p)) by FINSEQ_1:def 3;

        then ( len q) <= ( len p) by FINSEQ_1: 5;

        then m1 <= ( len p) by A4, XXREAL_0: 2;

        hence (q . n1) <> (q . m1) by A1, A2, A3, A5, A6, GRAPH_1:def 16;

      end;

      then p9 is Path of G by GRAPH_1:def 16;

      hence thesis;

    end;

    theorem :: GRAPH_4:23

    

     Th23: sc is OrientedPath of G

    proof

      assume not sc is OrientedPath of G;

      then

      consider m, n such that

       A1: 1 <= m and

       A2: m < n and

       A3: n <= ( len sc) and

       A4: (sc . m) = (sc . n) by GRAPH_1:def 16;

      sc is Simple by Th18;

      then

      consider vs such that

       A5: vs is_oriented_vertex_seq_of sc and

       A6: for n, m st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs);

      

       A7: ( len vs) = (( len sc) + 1) by A5;

      

       A8: m <= ( len sc) by A2, A3, XXREAL_0: 2;

      

       A9: 1 <= n by A1, A2, XXREAL_0: 2;

      

       A10: n <= ( len vs) by A3, A7, NAT_1: 12;

      

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

      

       A12: (n + 1) <= ( len vs) by A3, A7, XREAL_1: 6;

      

       A13: m < (n + 1) by A11, NAT_1: 12;

      set v1 = (vs /. m);

      set v2 = (vs /. (m + 1));

      

       A14: (sc . m) orientedly_joins (v1,v2) by A1, A5, A8;

      set v19 = (vs /. n);

      set v29 = (vs /. (n + 1));

      

       A15: (sc . n) orientedly_joins (v19,v29) by A3, A5, A9;

      then

       A16: v1 = v19 by A4, A14;

      

       A17: v2 = v29 by A4, A14, A15;

      

       A18: m <= ( len vs) by A12, A13, XXREAL_0: 2;

      

       A19: (m + 1) <= ( len vs) by A11, A12, XXREAL_0: 2;

      

       A20: v1 = (vs . m) by A1, A18, FINSEQ_4: 15;

      

       A21: v2 = (vs . (m + 1)) by A19, FINSEQ_4: 15, NAT_1: 12;

      

       A22: v19 = (vs . n) by A9, A10, FINSEQ_4: 15;

      

       A23: v29 = (vs . (n + 1)) by A12, FINSEQ_4: 15, NAT_1: 12;

      m = 1 by A1, A2, A6, A10, A16, A20, A22;

      hence contradiction by A6, A11, A12, A17, A21, A23;

    end;

    theorem :: GRAPH_4:24

    for c1 be FinSequence holds (c1 is Simple oriented Chain of G iff c1 is oriented simple Chain of G) & (c1 is oriented simple Chain of G implies c1 is OrientedPath of G) by Th18, Th19, Th23;