graph_2.miz



    begin

    

     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;

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

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

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

      end;

        suppose m <= n;

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

      end;

    end;

    ::$Canceled

    ::$Canceled

    reserve p,q for FinSequence,

X,Y,x,y,e for set,

D for non empty set,

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

    reserve G for Graph;

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

    theorem :: GRAPH_2:29

    e joins (v1,v2) implies e joins (v2,v1);

    theorem :: GRAPH_2:30

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

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

c,c1,c2 for Chain of G;

    definition

      let G, X;

      :: GRAPH_2:def1

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

      correctness ;

    end

    definition

      let G, vs;

      let c be FinSequence;

      :: GRAPH_2:def2

      pred vs is_vertex_seq_of c means ( len vs) = (( len c) + 1) & for n be Nat st 1 <= n & n <= ( len c) holds (c . n) joins ((vs /. n),(vs /. (n + 1)));

    end

    theorem :: GRAPH_2:31

    

     Th31: c <> {} & vs is_vertex_seq_of c implies (G -VSet ( rng c)) = ( rng vs)

    proof

      assume that

       A1: c <> {} and

       A2: vs is_vertex_seq_of c;

      

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

      now

        let y be object;

        hereby

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

          then

          consider v be Element of G such that

           A4: v = y and

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

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

           A6: e in ( rng c) and

           A7: v = (the Source of G . e) or v = (the Target of G . e) by A5;

          consider x be object such that

           A8: x in ( dom c) and

           A9: e = (c . x) by A6, FUNCT_1:def 3;

          reconsider x as Element of NAT by A8;

          

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

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

          set v1 = (vs /. x);

          

           A11: x <= ( len c) by A8, FINSEQ_3: 25;

          then

           A12: (x + 1) in ( dom vs) by A10, FINSEQ_3: 25, A3, XREAL_1: 7;

          

           A13: 1 <= x by A8, FINSEQ_3: 25;

          then (c . x) joins (v1,v2) by A2, A11;

          then

           A14: v = v1 or v = v2 by A7, A9;

          

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

          then

           A16: v1 = (vs . x) by A13, FINSEQ_4: 15;

          

           A17: x in ( dom vs) by A13, A15, FINSEQ_3: 25;

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

          hence y in ( rng vs) by A4, A16, A14, A17, A12, FUNCT_1:def 3;

        end;

        assume y in ( rng vs);

        then

        consider x be object such that

         A18: x in ( dom vs) and

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

        reconsider x as Element of NAT by A18;

        

         A20: 1 <= x by A18, FINSEQ_3: 25;

        

         A21: x <= ( len vs) by A18, FINSEQ_3: 25;

        per cases by A3, A21, NAT_1: 8;

          suppose

           A22: x <= ( len c);

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

          then

           A23: (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 A23;

          x in ( dom c) by A20, A22, FINSEQ_3: 25;

          then

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

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

          set v1 = (vs /. x);

          (c . x) joins (v1,v2) by A2, A20, A22;

          then

           A25: v1 = (the Source of G . e) & v2 = (the Target of G . e) or v2 = (the Source of G . e) & v1 = (the Target of G . e);

          v1 = (vs . x) by A20, A21, FINSEQ_4: 15;

          hence y in (G -VSet ( rng c)) by A19, A25, A24;

        end;

          suppose

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

          set l = ( len c);

          

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

          ( 0 + 1) = 1;

          then

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

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

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

          then

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

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

          set v1 = (vs /. l);

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

          then

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

          (c . l) joins (v1,v2) by A2, A28;

          then

           A30: v1 = (the Source of G . e) & v2 = (the Target of G . e) or v2 = (the Source of G . e) & v1 = (the Target of G . e);

          v2 = (vs . (l + 1)) by A3, A20, A26, FINSEQ_4: 15;

          hence y in (G -VSet ( rng c)) by A19, A26, A30, A29;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GRAPH_2:32

    

     Th32: <*v*> is_vertex_seq_of {} by FINSEQ_1: 40;

    theorem :: GRAPH_2:33

    

     Th33: ex vs st vs is_vertex_seq_of c

    proof

      consider p such that

       A1: ( len p) = (( len c) + 1) and

       A2: for n st 1 <= n & n <= ( len p) holds (p . n) in the carrier of G and

       A3: for n st 1 <= n & n <= ( len c) holds ex v1, v2 st v1 = (p . n) & v2 = (p . (n + 1)) & (c . n) joins (v1,v2) by GRAPH_1:def 14;

      ( rng p) c= the carrier of G

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be object such that

         A4: x in ( dom p) and

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

        reconsider n = x as Element of NAT by A4;

        

         A6: n <= ( len p) by A4, FINSEQ_3: 25;

        1 <= n by A4, FINSEQ_3: 25;

        hence thesis by A2, A5, A6;

      end;

      then

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

      take p;

      thus ( len p) = (( len c) + 1) by A1;

      let n be Nat;

      assume that

       A7: 1 <= n and

       A8: n <= ( len c);

      

       A9: n <= ( len p) by A1, A8, NAT_1: 12;

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

      then

       A10: (p /. (n + 1)) = (p . (n + 1)) by A1, A8, FINSEQ_4: 15, XREAL_1: 7;

      ex v1, v2 st v1 = (p . n) & v2 = (p . (n + 1)) & (c . n) joins (v1,v2) by A3, A7, A8;

      hence thesis by A7, A9, A10, FINSEQ_4: 15;

    end;

    theorem :: GRAPH_2:34

    

     Th34: c <> {} & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & vs1 <> vs2 implies (vs1 . 1) <> (vs2 . 1) & for vs st vs is_vertex_seq_of c holds vs = vs1 or vs = vs2

    proof

      assume that

       A1: c <> {} and

       A2: vs1 is_vertex_seq_of c and

       A3: vs2 is_vertex_seq_of c;

      

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

      defpred P[ Nat] means $1 in ( dom vs1) & (vs1 . $1) <> (vs2 . $1);

      set TG = the Target of G;

      set SG = the Source of G;

      

       A5: ( Seg ( len vs1)) = ( dom vs1) by FINSEQ_1:def 3;

      

       A6: ( Seg ( len vs2)) = ( dom vs2) by FINSEQ_1:def 3;

      

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

      assume vs1 <> vs2;

      then

       A8: ex j be Nat st P[j] by A4, A7, FINSEQ_2: 9;

      consider k be Nat such that

       A9: P[k] and

       A10: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A8);

      

       A11: 1 <= k by A9, FINSEQ_3: 25;

      per cases by A11, XXREAL_0: 1;

        suppose

         A12: k = 1;

        hence (vs1 . 1) <> (vs2 . 1) by A9;

        set v21 = (vs2 /. 1);

        set v12 = (vs1 /. (1 + 1));

        set v11 = (vs1 /. 1);

        let vs;

        set v1 = (vs /. 1);

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

        assume

         A13: vs is_vertex_seq_of c;

        then

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

        ( 0 + 1) = 1;

        then

         A15: 1 <= ( len c) by A1, NAT_1: 13;

        then

         A16: (c . 1) joins ((vs /. 1),(vs /. (1 + 1))) by A13;

        (c . 1) joins ((vs1 /. 1),(vs1 /. (1 + 1))) by A2, A15;

        then

         A17: v1 = v11 & v2 = v12 or v1 = v12 & v2 = v11 by A16;

        

         A18: 1 <= ( len vs1) by A4, NAT_1: 12;

        then

         A19: v11 = (vs1 . 1) by FINSEQ_4: 15;

        

         A20: v21 = (vs2 . 1) by A4, A7, A18, FINSEQ_4: 15;

        

         A21: (c . 1) joins ((vs2 /. 1),(vs2 /. (1 + 1))) by A3, A15;

        thus vs = vs1 or vs = vs2

        proof

          per cases by A9, A12, A19, A20, A16, A21, A17;

            suppose

             A22: v1 = v11;

            now

              defpred P[ Nat] means $1 in ( dom vs) implies (vs . $1) = (vs1 . $1);

              thus ( len vs) = ( len vs);

              thus ( len vs1) = ( len vs) by A4, A13;

              

               A23: for i be Nat st P[i] holds P[(i + 1)]

              proof

                

                 A24: ( 0 + 1) = 1;

                let i be Nat;

                assume

                 A25: i in ( dom vs) implies (vs . i) = (vs1 . i);

                assume

                 A26: (i + 1) in ( dom vs);

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

                

                 A27: 1 <= (i + 1) by A26, FINSEQ_3: 25;

                

                 A28: (i + 1) <= ( len vs) by A26, FINSEQ_3: 25;

                per cases by A24, NAT_1: 13;

                  suppose i = 0 ;

                  hence thesis by A4, A14, A18, A19, A22, FINSEQ_4: 15;

                end;

                  suppose

                   A29: 1 <= i;

                  set v12 = (vs1 /. (i + 1));

                  set v11 = (vs1 /. i);

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

                  

                   A30: v2 = (vs . (i + 1)) by A27, A28, FINSEQ_4: 15;

                  set v1 = (vs /. i);

                  

                   A31: i <= ( len c) by A14, A28, XREAL_1: 6;

                  then

                   A32: (c . i) joins ((vs1 /. i),(vs1 /. (i + 1))) by A2, A29;

                  

                   A33: i <= ( len vs) by A14, A31, NAT_1: 12;

                  then

                   A34: v1 = (vs . i) by A29, FINSEQ_4: 15;

                  (c . i) joins ((vs /. i),(vs /. (i + 1))) by A13, A29, A31;

                  then

                   A35: v1 = v11 & v2 = v12 or v1 = v12 & v2 = v11 by A32;

                  v11 = (vs1 . i) by A4, A14, A29, A33, FINSEQ_4: 15;

                  hence thesis by A4, A14, A25, A27, A28, A29, A33, A34, A30, A35, FINSEQ_3: 25, FINSEQ_4: 15;

                end;

              end;

              

               A36: P[ 0 ] by FINSEQ_3: 25;

              thus for i be Nat holds P[i] from NAT_1:sch 2( A36, A23);

            end;

            hence thesis by FINSEQ_2: 9;

          end;

            suppose

             A37: v1 = v21;

            now

              defpred P[ Nat] means $1 in ( dom vs) implies (vs . $1) = (vs2 . $1);

              thus ( len vs) = ( len vs);

              thus ( len vs2) = ( len vs) by A7, A13;

              

               A38: for i be Nat st P[i] holds P[(i + 1)]

              proof

                

                 A39: ( 0 + 1) = 1;

                let i be Nat;

                assume

                 A40: i in ( dom vs) implies (vs . i) = (vs2 . i);

                assume

                 A41: (i + 1) in ( dom vs);

                then

                 A42: 1 <= (i + 1) by FINSEQ_3: 25;

                

                 A43: (i + 1) <= ( len vs) by A41, FINSEQ_3: 25;

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

                per cases by A39, NAT_1: 13;

                  suppose i = 0 ;

                  hence thesis by A4, A14, A18, A20, A37, FINSEQ_4: 15;

                end;

                  suppose

                   A44: 1 <= i;

                  set v12 = (vs2 /. (i + 1));

                  set v11 = (vs2 /. i);

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

                  

                   A45: v2 = (vs . (i + 1)) by A42, A43, FINSEQ_4: 15;

                  set v1 = (vs /. i);

                  

                   A46: i <= ( len c) by A14, A43, XREAL_1: 6;

                  then

                   A47: (c . i) joins ((vs2 /. i),(vs2 /. (i + 1))) by A3, A44;

                  

                   A48: i <= ( len vs) by A14, A46, NAT_1: 12;

                  then

                   A49: v1 = (vs . i) by A44, FINSEQ_4: 15;

                  (c . i) joins ((vs /. i),(vs /. (i + 1))) by A13, A44, A46;

                  then

                   A50: v1 = v11 & v2 = v12 or v1 = v12 & v2 = v11 by A47;

                  v11 = (vs2 . i) by A7, A14, A44, A48, FINSEQ_4: 15;

                  hence thesis by A7, A14, A40, A42, A43, A44, A48, A49, A45, A50, FINSEQ_3: 25, FINSEQ_4: 15;

                end;

              end;

              

               A51: P[ 0 ] by FINSEQ_3: 25;

              thus for i be Nat holds P[i] from NAT_1:sch 2( A51, A38);

            end;

            hence thesis by FINSEQ_2: 9;

          end;

        end;

      end;

        suppose 1 < k;

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

        then

        consider k1 be Nat such that

         A52: 1 <= k1 and

         A53: k1 < k and

         A54: k = (k1 + 1) by FINSEQ_6: 127;

        

         A55: k <= ( len vs1) by A9, FINSEQ_3: 25;

        then

         A56: k1 <= ( len vs1) by A53, XXREAL_0: 2;

        then

         A57: k1 in ( dom vs1) by A52, FINSEQ_3: 25;

        

         A58: (vs1 /. k1) = (vs1 . k1) by A52, A56, FINSEQ_4: 15;

        

         A59: (vs2 /. k) = (vs2 . k) by A4, A7, A5, A6, A9, PARTFUN1:def 6;

        

         A60: (vs1 /. k) = (vs1 . k) by A9, PARTFUN1:def 6;

        

         A61: k1 <= ( len c) by A4, A54, A55, XREAL_1: 6;

        then (c . k1) joins ((vs1 /. k1),(vs1 /. (k1 + 1))) by A2, A52;

        then

         A62: (SG . (c . k1)) = (vs1 /. k1) & (TG . (c . k1)) = (vs1 /. k) or (SG . (c . k1)) = (vs1 /. k) & (TG . (c . k1)) = (vs1 /. k1) by A54;

        (c . k1) joins ((vs2 /. k1),(vs2 /. (k1 + 1))) by A3, A52, A61;

        then

         A63: (SG . (c . k1)) = (vs2 /. k1) & (TG . (c . k1)) = (vs2 /. k) or (SG . (c . k1)) = (vs2 /. k) & (TG . (c . k1)) = (vs2 /. k1) by A54;

        (vs2 /. k1) = (vs2 . k1) by A4, A7, A52, A56, FINSEQ_4: 15;

        hence thesis by A9, A10, A53, A57, A58, A60, A59, A62, A63;

      end;

    end;

    definition

      let G;

      let c be FinSequence;

      :: GRAPH_2:def3

      pred c alternates_vertices_in G means ( len c) >= 1 & ( card (G -VSet ( rng c))) = 2 & for n st n in ( dom c) holds (the Source of G . (c . n)) <> (the Target of G . (c . n));

    end

    theorem :: GRAPH_2:35

    

     Th35: c alternates_vertices_in G & vs is_vertex_seq_of c implies for k st k in ( dom c) holds (vs . k) <> (vs . (k + 1))

    proof

      assume that

       A1: c alternates_vertices_in G and

       A2: vs is_vertex_seq_of c;

      set TG = the Target of G;

      set SG = the Source of G;

      let k;

      set px = (vs /. k);

      set px1 = (vs /. (k + 1));

      assume

       A3: k in ( dom c);

      then

       A4: k <= ( len c) by FINSEQ_3: 25;

      

       A5: 1 <= k by A3, FINSEQ_3: 25;

      then (c . k) joins (px,px1) by A2, A4;

      then

       A6: (TG . (c . k)) = px1 & (SG . (c . k)) = px or (TG . (c . k)) = px & (SG . (c . k)) = px1;

      

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

      then k <= ( len vs) by A4, NAT_1: 12;

      then

       A8: px = (vs . k) by A5, FINSEQ_4: 15;

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

      then px1 = (vs . (k + 1)) by A4, A7, FINSEQ_4: 15, XREAL_1: 7;

      hence thesis by A1, A3, A8, A6;

    end;

    theorem :: GRAPH_2:36

    

     Th36: c alternates_vertices_in G & vs is_vertex_seq_of c implies ( rng vs) = {(the Source of G . (c . 1)), (the Target of G . (c . 1))}

    proof

      assume that

       A1: c alternates_vertices_in G and

       A2: vs is_vertex_seq_of c;

      set px1 = (vs /. (1 + 1));

      set TG = the Target of G;

      set SG = the Source of G;

      set px = (vs /. 1);

      

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

      then

       A4: 1 <= ( len vs) by NAT_1: 12;

      then

       A5: px = (vs . 1) by FINSEQ_4: 15;

      c <> {} by A1;

      then ( card ( rng vs)) = 2 by A1, A2, Th31;

      then

      consider x,y be object such that x <> y and

       A6: ( rng vs) = {x, y} by CARD_2: 60;

      1 in ( dom vs) by A4, FINSEQ_3: 25;

      then (vs . 1) in ( rng vs) by FUNCT_1:def 3;

      then

       A7: (vs . 1) = x or (vs . 1) = y by A6, TARSKI:def 2;

      

       A8: 1 <= ( len c) by A1;

      then

       A9: 1 in ( dom c) by FINSEQ_3: 25;

      

       A10: px1 = (vs . (1 + 1)) by A8, A3, FINSEQ_4: 15, XREAL_1: 7;

      (c . 1) joins (px,px1) by A2, A8;

      then

       A11: (TG . (c . 1)) = px1 & (SG . (c . 1)) = px or (TG . (c . 1)) = px & (SG . (c . 1)) = px1;

      (1 + 1) in ( dom vs) by FINSEQ_3: 25, A8, A3, XREAL_1: 7;

      then (vs . (1 + 1)) in ( rng vs) by FUNCT_1:def 3;

      then (vs . (1 + 1)) = x or (vs . (1 + 1)) = y by A6, TARSKI:def 2;

      hence thesis by A1, A6, A5, A10, A11, A7, A9;

    end;

    theorem :: GRAPH_2:37

    

     Th37: c alternates_vertices_in G & vs is_vertex_seq_of c implies vs is TwoValued Alternating FinSequence

    proof

      assume that

       A1: c alternates_vertices_in G and

       A2: vs is_vertex_seq_of c;

      

       A3: c <> {} by A1;

      

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

       A5:

      now

        let k be Nat;

        assume that

         A6: 1 <= k and

         A7: (k + 1) <= ( len vs);

        k <= ( len c) by A4, A7, XREAL_1: 6;

        hence (vs . k) <> (vs . (k + 1)) by A1, A2, Th35, A6, FINSEQ_3: 25;

      end;

      ( card ( rng vs)) = 2 by A2, A3, Th31, A1;

      hence thesis by A5, FINSEQ_6:def 6, FINSEQ_6:def 7;

    end;

    theorem :: GRAPH_2:38

    

     Th38: c alternates_vertices_in G implies ex vs1, vs2 st vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & for vs st vs is_vertex_seq_of c holds vs = vs1 or vs = vs2

    proof

      set X = (the Source of G . (c . 1));

      set Y = (the Target of G . (c . 1));

      consider p1 be FinSequence of the carrier of G such that

       A1: p1 is_vertex_seq_of c by Th33;

      assume

       A2: c alternates_vertices_in G;

      then

       A3: 1 <= ( len c);

      then

       A4: 1 in ( dom c) by FINSEQ_3: 25;

      

       A5: (1 + 1) = 2;

      then

       A6: (p1 . 1) <> (p1 . 2) by A2, A1, A4, Th35;

      

       A7: ( rng p1) = {X, Y} by A2, A1, Th36;

      

       A8: ( len p1) = (( len c) + 1) by A1;

      then

       A9: ( len p1) > 1 by A3, NAT_1: 13;

      then

      consider p2 be TwoValued Alternating FinSequence such that

       A10: ( rng p2) = {(p1 . 2), (p1 . 1)} and

       A11: ( len p2) = ( len p1) and

       A12: (p2 . 1) = (p1 . 2) by A6, FINSEQ_6: 149;

      

       A13: ( dom p1) = ( dom p2) by A11, FINSEQ_3: 29;

      (1 + 1) <= ( len p1) by A9, NAT_1: 13;

      then 2 in ( dom p1) by FINSEQ_3: 25;

      then (p1 . 2) in ( rng p1) by FUNCT_1:def 3;

      then

       A14: (p1 . 2) = X or (p1 . 2) = Y by A7, TARSKI:def 2;

      1 in ( dom p1) by A9, FINSEQ_3: 25;

      then (p1 . 1) in ( rng p1) by FUNCT_1:def 3;

      then

       A15: (p1 . 1) = X or (p1 . 1) = Y by A7, TARSKI:def 2;

      then

      reconsider p2 as FinSequence of the carrier of G by A2, A1, A7, A4, A5, A10, A14, Th35, FINSEQ_1:def 4;

      take p1, p2;

      thus p1 <> p2 by A2, A1, A4, A5, A12, Th35;

      thus p1 is_vertex_seq_of c by A1;

      

       A16: p1 is TwoValued Alternating FinSequence by A2, A1, Th37;

      now

        thus ( len p2) = (( len c) + 1) by A1, A11;

        let n be Nat such that

         A17: 1 <= n and

         A18: n <= ( len c);

        

         A19: n <= ( len p1) by A8, A18, NAT_1: 12;

        then

         A20: (p2 /. n) = (p2 . n) by A11, A17, FINSEQ_4: 15;

        

         A21: n in ( dom p1) by A17, A19, FINSEQ_3: 25;

        then (p2 . n) in {X, Y} by A2, A1, A4, A5, A10, A13, A15, A14, Th35, FUNCT_1:def 3;

        then

         A22: (p2 . n) = X or (p2 . n) = Y by TARSKI:def 2;

        set x = (p1 /. n);

        set y = (p1 /. (n + 1));

        

         A23: (c . n) joins (x,y) by A1, A17, A18;

        

         A24: (n + 1) <= ( len p1) by A8, A18, XREAL_1: 6;

        then

         A25: (p2 /. (n + 1)) = (p2 . (n + 1)) by A11, FINSEQ_4: 15, NAT_1: 12;

        

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

        then

         A27: (n + 1) in ( dom p1) by A24, FINSEQ_3: 25;

        then (p2 . (n + 1)) in {X, Y} by A2, A1, A4, A5, A10, A13, A15, A14, Th35, FUNCT_1:def 3;

        then

         A28: (p2 . (n + 1)) = X or (p2 . (n + 1)) = Y by TARSKI:def 2;

        (p1 . n) in {X, Y} by A7, A21, FUNCT_1:def 3;

        then (p1 . n) = X or (p1 . n) = Y by TARSKI:def 2;

        then

         A29: x = (p2 . (n + 1)) by A7, A16, A6, A10, A11, A12, A15, A14, A17, A19, A24, A22, A28, FINSEQ_6:def 7, FINSEQ_6: 147, FINSEQ_4: 15;

        (p1 . (n + 1)) in {X, Y} by A7, A27, FUNCT_1:def 3;

        then (p1 . (n + 1)) = X or (p1 . (n + 1)) = Y by TARSKI:def 2;

        then y = (p2 . n) by A7, A16, A6, A10, A11, A12, A15, A14, A17, A26, A24, A22, A28, FINSEQ_6:def 7, FINSEQ_6: 147, FINSEQ_4: 15;

        hence (c . n) joins ((p2 /. n),(p2 /. (n + 1))) by A23, A29, A20, A25;

      end;

      hence p2 is_vertex_seq_of c;

      let p be FinSequence of the carrier of G;

      assume

       A30: p is_vertex_seq_of c;

      then

      reconsider p9 = p as TwoValued Alternating FinSequence by A2, Th37;

      

       A31: ( len p) = (( len c) + 1) by A30;

      ( rng p) = {X, Y} by A2, A30, Th36;

      then p9 = p1 or p9 = p2 by A8, A7, A16, A6, A10, A11, A12, A15, A14, A31, FINSEQ_6: 148;

      hence thesis;

    end;

    

     Lm7: (for x, y st x in D & y in D holds x = y) implies ( card D) = 1

    proof

      set x = the Element of D;

      assume for x, y st x in D & y in D holds x = y;

      then for y be object holds y in D iff y = x;

      then D = {x} by TARSKI:def 1;

      hence thesis by CARD_2: 42;

    end;

    theorem :: GRAPH_2:39

    

     Th39: vs is_vertex_seq_of c implies (( card the carrier of G) = 1 or c <> {} & not c alternates_vertices_in G iff for vs1 st vs1 is_vertex_seq_of c holds vs1 = vs)

    proof

      assume

       A1: vs is_vertex_seq_of c;

      hereby

        assume

         A2: ( card the carrier of G) = 1 or c <> {} & not c alternates_vertices_in G;

        per cases by A2;

          suppose

           A3: ( card the carrier of G) = 1;

          then

          reconsider tVG = the carrier of G as finite set;

          consider X be object such that

           A4: tVG = {X} by A3, CARD_2: 42;

          

           A5: ( rng vs) c= {X} by A4, FINSEQ_1:def 4;

          

           A6: ( len vs) = (( len c) + 1) by A1;

          let vs1;

          

           A7: ( Seg ( len vs)) = ( dom vs) by FINSEQ_1:def 3;

          assume vs1 is_vertex_seq_of c;

          then

           A8: ( len vs1) = (( len c) + 1);

          assume vs1 <> vs;

          then

          consider j be Nat such that

           A9: j in ( dom vs) and

           A10: (vs1 . j) <> (vs . j) by A8, A6, FINSEQ_2: 9;

          (vs . j) in ( rng vs) by A9, FUNCT_1:def 3;

          then

           A11: (vs . j) = X by A5, TARSKI:def 1;

          

           A12: ( rng vs1) c= {X} by A4, FINSEQ_1:def 4;

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

          then (vs1 . j) in ( rng vs1) by A8, A6, A7, A9, FUNCT_1:def 3;

          hence contradiction by A10, A12, A11, TARSKI:def 1;

        end;

          suppose

           A13: c <> {} & not c alternates_vertices_in G;

          thus for vs1 st vs1 is_vertex_seq_of c holds vs1 = vs

          proof

            set TG = the Target of G;

            set SG = the Source of G;

            let vs1;

            defpred P[ Nat] means $1 in ( dom vs1) & (vs1 . $1) <> (vs . $1);

            assume

             A14: vs1 is_vertex_seq_of c;

            then

             A15: ( len vs1) = (( len c) + 1);

            

             A16: ( len vs) = (( len c) + 1) by A1;

            then

             A17: ( dom vs1) = ( dom vs) by A15, FINSEQ_3: 29;

            assume vs1 <> vs;

            then

             A18: ex i be Nat st P[i] by A15, A16, FINSEQ_2: 9;

            consider k be Nat such that

             A19: P[k] and

             A20: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A18);

            

             A21: ( 0 + 1) = 1 & k = 0 or ( 0 + 1) <= k by NAT_1: 13;

            per cases by A21, XXREAL_0: 1;

              suppose k = 0 ;

              hence contradiction by A19, FINSEQ_3: 25;

            end;

              suppose

               A22: k = 1;

              thus contradiction

              proof

                

                 A23: ( 0 + 1) = 1;

                per cases by A23, NAT_1: 13;

                  suppose ( len c) = 0 ;

                  hence contradiction by A13;

                end;

                  suppose

                   A24: 1 <= ( len c);

                  defpred P[ Nat] means $1 in ( dom c) implies (vs1 /. $1) <> (vs /. $1) & (vs1 /. ($1 + 1)) <> (vs /. ($1 + 1)) & ((TG . (c . $1)) = (TG . (c . 1)) & (SG . (c . $1)) = (SG . (c . 1)) or (TG . (c . $1)) = (SG . (c . 1)) & (SG . (c . $1)) = (TG . (c . 1)));

                  

                   A25: (vs /. k) = (vs . k) by A17, A19, PARTFUN1:def 6;

                  

                   A26: (vs1 /. k) = (vs1 . k) by A19, PARTFUN1:def 6;

                   A27:

                  now

                    let n be Nat;

                    assume

                     A28: P[n];

                    thus P[(n + 1)]

                    proof

                      assume

                       A29: (n + 1) in ( dom c);

                      then

                       A30: 1 <= (n + 1) by FINSEQ_3: 25;

                      

                       A31: (n + 1) <= ( len c) by A29, FINSEQ_3: 25;

                      thus (vs1 /. (n + 1)) <> (vs /. (n + 1)) & (vs1 /. ((n + 1) + 1)) <> (vs /. ((n + 1) + 1)) & ((TG . (c . (n + 1))) = (TG . (c . 1)) & (SG . (c . (n + 1))) = (SG . (c . 1)) or (TG . (c . (n + 1))) = (SG . (c . 1)) & (SG . (c . (n + 1))) = (TG . (c . 1)))

                      proof

                        per cases ;

                          suppose

                           A32: n = 0 ;

                          hence (vs1 /. (n + 1)) <> (vs /. (n + 1)) by A17, A19, A22, A26, PARTFUN1:def 6;

                          

                           A33: 1 <= ( len c) by A30, A31, XXREAL_0: 2;

                          then (c . 1) joins ((vs /. 1),(vs /. (1 + 1))) by A1;

                          then

                           A34: (SG . (c . 1)) = (vs /. 1) & (TG . (c . 1)) = (vs /. (1 + 1)) or (SG . (c . 1)) = (vs /. (1 + 1)) & (TG . (c . 1)) = (vs /. 1);

                          (c . 1) joins ((vs1 /. 1),(vs1 /. (1 + 1))) by A14, A33;

                          hence (vs1 /. ((n + 1) + 1)) <> (vs /. ((n + 1) + 1)) by A17, A19, A22, A26, A32, A34, PARTFUN1:def 6;

                          thus thesis by A32;

                        end;

                          suppose

                           A35: 0 < n;

                          

                           A36: n <= ( len c) by A31, NAT_1: 13;

                          

                           A37: ( 0 + 1) <= n by A35, NAT_1: 13;

                          hence (vs1 /. (n + 1)) <> (vs /. (n + 1)) by A28, A36, FINSEQ_3: 25;

                          (c . n) joins ((vs1 /. n),(vs1 /. (n + 1))) by A14, A37, A36;

                          then

                           A38: (SG . (c . n)) = (vs1 /. n) & (TG . (c . n)) = (vs1 /. (n + 1)) or (SG . (c . n)) = (vs1 /. (n + 1)) & (TG . (c . n)) = (vs1 /. n);

                          (c . (n + 1)) joins ((vs /. (n + 1)),(vs /. ((n + 1) + 1))) by A1, A30, A31;

                          then

                           A39: (SG . (c . (n + 1))) = (vs /. (n + 1)) & (TG . (c . (n + 1))) = (vs /. ((n + 1) + 1)) or (SG . (c . (n + 1))) = (vs /. ((n + 1) + 1)) & (TG . (c . (n + 1))) = (vs /. (n + 1));

                          

                           A40: (c . (n + 1)) joins ((vs1 /. (n + 1)),(vs1 /. ((n + 1) + 1))) by A14, A30, A31;

                          hence (vs1 /. ((n + 1) + 1)) <> (vs /. ((n + 1) + 1)) by A28, A37, A36, A39, FINSEQ_3: 25;

                          (c . n) joins ((vs /. n),(vs /. (n + 1))) by A1, A37, A36;

                          hence thesis by A28, A37, A36, A38, A40, A39, FINSEQ_3: 25;

                        end;

                      end;

                    end;

                  end;

                  

                   A41: P[ 0 ] by FINSEQ_3: 25;

                  

                   A42: for n be Nat holds P[n] from NAT_1:sch 2( A41, A27);

                  now

                    let x be object;

                    hereby

                      assume x in (G -VSet ( rng c));

                      then

                      consider v such that

                       A43: x = v and

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

                      consider e such that

                       A45: e in ( rng c) and

                       A46: v = (SG . e) or v = (TG . e) by A44;

                      consider d be object such that

                       A47: d in ( dom c) and

                       A48: e = (c . d) by A45, FUNCT_1:def 3;

                      reconsider d as Element of NAT by A47;

                      (TG . (c . d)) = (TG . (c . 1)) & (SG . (c . d)) = (SG . (c . 1)) or (TG . (c . d)) = (SG . (c . 1)) & (SG . (c . d)) = (TG . (c . 1)) by A42, A47;

                      hence x in {(SG . (c . 1)), (TG . (c . 1))} by A43, A46, A48, TARSKI:def 2;

                    end;

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

                    then

                     A49: 1 in ( dom c) by FINSEQ_3: 25;

                    then

                     A50: (c . 1) in ( rng c) by FUNCT_1:def 3;

                    

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

                    then

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

                    reconsider t = (TG . e) as Element of G by A50, A51, FUNCT_2: 5;

                    reconsider s = (SG . e) as Element of G by A50, A51, FUNCT_2: 5;

                    assume x in {(SG . (c . 1)), (TG . (c . 1))};

                    then

                     A52: x = s or x = t by TARSKI:def 2;

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

                    hence x in (G -VSet ( rng c)) by A52;

                  end;

                  then

                   A53: (G -VSet ( rng c)) = {(SG . (c . 1)), (TG . (c . 1))} by TARSKI: 2;

                  (c . k) joins ((vs1 /. k),(vs1 /. (k + 1))) by A14, A22, A24;

                  then

                   A54: (SG . (c . 1)) = (vs1 /. 1) & (TG . (c . 1)) = (vs1 /. (k + 1)) or (SG . (c . 1)) = (vs1 /. (k + 1)) & (TG . (c . 1)) = (vs1 /. 1) by A22;

                  

                   A55: (c . k) joins ((vs /. k),(vs /. (k + 1))) by A1, A22, A24;

                   A56:

                  now

                    let n;

                    n in ( dom c) implies (TG . (c . n)) = (TG . (c . 1)) & (SG . (c . n)) = (SG . (c . 1)) or (TG . (c . n)) = (SG . (c . 1)) & (SG . (c . n)) = (TG . (c . 1)) by A42;

                    hence n in ( dom c) implies (SG . (c . n)) <> (TG . (c . n)) by A19, A22, A26, A25, A55, A54;

                  end;

                  (SG . (c . 1)) = (vs /. 1) & (TG . (c . 1)) = (vs /. (k + 1)) or (SG . (c . 1)) = (vs /. (k + 1)) & (TG . (c . 1)) = (vs /. 1) by A22, A55;

                  then ( card (G -VSet ( rng c))) = 2 by A19, A22, A26, A25, A54, A53, CARD_2: 57;

                  hence contradiction by A13, A24, A56;

                end;

              end;

            end;

              suppose 1 < k;

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

              then

              consider k1 be Nat such that

               A57: 1 <= k1 and

               A58: k1 < k and

               A59: k = (k1 + 1) by FINSEQ_6: 127;

              

               A60: k <= ( len vs1) by A19, FINSEQ_3: 25;

              then

               A61: k1 <= ( len vs1) by A58, XXREAL_0: 2;

              then

               A62: k1 in ( dom vs1) by A57, FINSEQ_3: 25;

              

               A63: k1 <= ( len c) by A15, A59, A60, XREAL_1: 6;

              then (c . k1) joins ((vs1 /. k1),(vs1 /. (k1 + 1))) by A14, A57;

              then

               A64: (SG . (c . k1)) = (vs1 /. k1) & (TG . (c . k1)) = (vs1 /. k) or (SG . (c . k1)) = (vs1 /. k) & (TG . (c . k1)) = (vs1 /. k1) by A59;

              

               A65: (vs1 /. k1) = (vs1 . k1) by A57, A61, FINSEQ_4: 15;

              

               A66: (vs1 /. k) = (vs1 . k) by A19, PARTFUN1:def 6;

              (c . k1) joins ((vs /. k1),(vs /. (k1 + 1))) by A1, A57, A63;

              then

               A67: (SG . (c . k1)) = (vs /. k1) & (TG . (c . k1)) = (vs /. k) or (SG . (c . k1)) = (vs /. k) & (TG . (c . k1)) = (vs /. k1) by A59;

              

               A68: (vs /. k) = (vs . k) by A17, A19, PARTFUN1:def 6;

              (vs /. k1) = (vs . k1) by A15, A16, A57, A61, FINSEQ_4: 15;

              hence contradiction by A19, A20, A58, A62, A65, A66, A68, A64, A67;

            end;

          end;

        end;

      end;

      assume

       A69: for vs1 st vs1 is_vertex_seq_of c holds vs1 = vs;

      assume ( card the carrier of G) <> 1;

      then

      consider x, y such that

       A70: x in the carrier of G and

       A71: y in the carrier of G and

       A72: x <> y by Lm7;

      reconsider y as Element of G by A71;

      reconsider x as Element of G by A70;

      assume

       A73: c = {} or c alternates_vertices_in G;

      thus contradiction

      proof

        per cases by A73;

          suppose

           A74: c = {} ;

          then <*x*> = vs by A69, Th32;

          then

           A75: (vs . 1) = x by FINSEQ_1: 40;

           <*y*> = vs by A69, A74, Th32;

          hence contradiction by A72, A75, FINSEQ_1: 40;

        end;

          suppose c alternates_vertices_in G;

          then

          consider vs1, vs2 such that

           A76: vs1 <> vs2 and

           A77: vs1 is_vertex_seq_of c and

           A78: vs2 is_vertex_seq_of c and for vs st vs is_vertex_seq_of c holds vs = vs1 or vs = vs2 by Th38;

          vs1 = vs by A69, A77;

          hence contradiction by A69, A76, A78;

        end;

      end;

    end;

    definition

      let G, c;

      assume

       A1: ( card the carrier of G) = 1 or c <> {} & not c alternates_vertices_in G;

      :: GRAPH_2:def4

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

      existence by Th33;

      uniqueness by A1, Th39;

    end

    theorem :: GRAPH_2:40

    

     Th40: vs is_vertex_seq_of c & c1 = (c | ( Seg n)) & vs1 = (vs | ( Seg (n + 1))) implies vs1 is_vertex_seq_of c1

    proof

      assume

       A1: vs is_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;

          then

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

          

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

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

          let k be Nat;

          assume that

           A9: 1 <= k and

           A10: k <= ( len c1);

          

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

          then

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

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

          then (k + 1) in ( Seg (n + 1)) by A8, A11;

          then

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

          

           A14: k <= ( len c) by A5, A8, A10, XXREAL_0: 2;

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

          then

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

          

           A16: k <= (n + 1) by A8, A10, NAT_1: 12;

          then

           A17: (vs1 /. k) = (vs1 . k) by A7, A9, FINSEQ_4: 15;

          k in ( Seg n) by A8, A9, A10;

          then

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

          k in ( Seg (n + 1)) by A9, A16;

          then

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

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

          hence (c1 . k) joins ((vs1 /. k),(vs1 /. (k + 1))) by A1, A9, A14, A18, A19, A13, A15, A17, A12;

        end;

          suppose

           A20: ( len c) <= n;

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

          then

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

          c1 = c by A3, A20, FINSEQ_2: 20;

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

        end;

      end;

      hence thesis;

    end;

    theorem :: GRAPH_2:41

    

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

    proof

      assume that

       A1: 1 <= m and

       A2: m <= n and

       A3: n <= ( len c);

      

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

      consider vs such that

       A5: vs is_vertex_seq_of c by Th33;

      set p9 = ((m,(n + 1)) -cut vs);

       A6:

      now

        let k be Nat;

        assume that

         A7: 1 <= k and

         A8: k <= ( len p9);

        k in ( dom p9) by A7, A8, FINSEQ_3: 25;

        then

         A9: (p9 . k) in ( rng p9) by FUNCT_1:def 3;

        

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

        ( rng p9) c= ( rng vs) by FINSEQ_6: 137;

        hence (p9 . k) in the carrier of G by A10, A9;

      end;

      assume

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

      then

       A12: ((( len q) + m) - m) = ((n + 1) - m) by A1, A3, A4, Lm2;

      

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

      then

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

      then

       A15: ((( len p9) + m) - m) = (((n + 1) + 1) - m) by A1, A4, FINSEQ_6:def 4;

      then

       A16: ( len p9) = (((n - m) + 1) + 1);

       A17:

      now

        (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 ;

        let k be Nat;

        reconsider i = (m1 + k) as Nat;

        assume that

         A18: 1 <= k and

         A19: k <= ( len q);

        ( 0 + 1) <= k by A18;

        then

        consider j such that 0 <= j and

         A20: j < ( len q) and

         A21: k = (j + 1) by A19, FINSEQ_6: 127;

        

         A22: (j + 1) < ( len p9) by A12, A16, A20, XREAL_1: 6;

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

        then

         A23: (p9 . (k + 1)) = (vs . (i + 1)) by A1, A4, A14, A22, FINSEQ_6:def 4;

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

        set v1 = (vs /. i);

        

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

        

         A25: i = (m + j) by A21;

        j < ( len p9) by A12, A16, A20, NAT_1: 13;

        then

         A26: (p9 . k) = (vs . i) by A1, A4, A14, A25, A22, FINSEQ_6:def 4;

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

        then

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

        then

         A28: i <= ( len vs) by A13, NAT_1: 12;

        take v1, v2;

        

         A29: (i + 1) <= ( len vs) by A13, A27, XREAL_1: 7;

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

        then

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

        then (c . i) joins (v1,v2) by A5, A27;

        hence v1 = (p9 . k) & v2 = (p9 . (k + 1)) & (q . k) joins (v1,v2) by A1, A3, A11, A4, A20, A21, A25, A30, A28, A24, A29, A26, A23, Lm2, FINSEQ_4: 15;

      end;

      thus q is Chain of G

      proof

        hereby

          let k be Nat;

          assume that

           A31: 1 <= k and

           A32: k <= ( len q);

          k in ( dom q) by A31, A32, FINSEQ_3: 25;

          then

           A33: (q . k) in ( rng q) by FUNCT_1:def 3;

          ( rng q) c= ( rng c) by A11, FINSEQ_6: 137;

          then

           A34: (q . k) in ( rng c) by A33;

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

          hence (q . k) in the carrier' of G by A34;

        end;

        take p9;

        thus ( len p9) = (( len q) + 1) by A12, A15;

        thus for n st 1 <= n & n <= ( len p9) holds (p9 . n) in the carrier of G by A6;

        thus thesis by A17;

      end;

    end;

    theorem :: GRAPH_2:42

    

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

    proof

      assume that

       A1: 1 <= m and

       A2: m <= n and

       A3: n <= ( len c);

      

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

      assume

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

      then

       A6: (( len c1) + m) = (n + 1) by A1, A3, A4, Lm2;

      assume that

       A7: vs is_vertex_seq_of c and

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

      

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

      then

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

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

      hence

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

      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);

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

      then

       A16: (vs1 . k) = (vs . i) by A1, A8, A4, A10, A15, FINSEQ_6:def 4;

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

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

      then

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

      then i <= ( len vs) by A9, NAT_1: 12;

      then

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

      

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

      then

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

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

      then

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

      ( 0 + 1) = 1;

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

      then

       A22: (vs1 /. k) = (vs1 . k) by A20, FINSEQ_4: 15;

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

      set v1 = (vs /. i);

      

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

      1 <= i by A1, NAT_1: 12;

      then

       A24: (c . i) joins (v1,v2) by A7, A17;

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

      then

       A25: (vs /. (i + 1)) = (vs . (i + 1)) by A9, A17, FINSEQ_4: 15, XREAL_1: 7;

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

      then (vs1 . (k + 1)) = (vs . (i + 1)) by A1, A8, A4, A10, A15, A23, FINSEQ_6:def 4;

      hence thesis by A1, A3, A5, A4, A14, A15, A24, A16, A18, A25, A22, A21, Lm2;

    end;

    theorem :: GRAPH_2:43

    

     Th43: vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & (vs1 . ( len vs1)) = (vs2 . 1) implies (c1 ^ c2) is Chain of G

    proof

      assume that

       A1: vs1 is_vertex_seq_of c1 and

       A2: vs2 is_vertex_seq_of c2 and

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

      set q = (c1 ^ c2);

      set p = (vs1 ^' vs2);

      

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

      then vs2 <> {} ;

      then

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

       A6:

      now

        let n be Nat such that

         A7: 1 <= n and

         A8: n <= ( len p);

        per cases ;

          suppose

           A9: n <= ( len vs1);

          then

           A10: n in ( dom vs1) by A7, FINSEQ_3: 25;

          (p . n) = (vs1 . n) by A7, A9, FINSEQ_6: 140;

          hence (p . n) in the carrier of G by A10, FINSEQ_2: 11;

        end;

          suppose

           A11: n > ( len vs1);

          then

          consider m be Nat such that

           A12: n = (( len vs1) + m) by NAT_1: 10;

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

          m <> 0 by A11, A12;

          then

           A13: ( 0 + 1) <= m by NAT_1: 13;

          (( len vs1) + m) <= (( len vs1) + (( len vs2) - 1)) by A5, A8, A12;

          then m <= (( len vs2) - 1) by XREAL_1: 6;

          then

           A14: (m + 1) <= ((( len vs2) - 1) + 1) by XREAL_1: 6;

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

          then

           A15: (m + 1) in ( dom vs2) by A14, FINSEQ_3: 25;

          m < ( len vs2) by A14, NAT_1: 13;

          then (p . (( len vs1) + m)) = (vs2 . (m + 1)) by A13, FINSEQ_6: 141;

          hence (p . n) in the carrier of G by A12, A15, FINSEQ_2: 11;

        end;

      end;

      

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

       A17:

      now

        let n be Nat;

        assume that

         A18: 1 <= n and

         A19: n <= ( len q);

        

         A20: n in ( dom q) by A18, A19, FINSEQ_3: 25;

        per cases by A20, FINSEQ_1: 25;

          suppose

           A21: n in ( dom c1);

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

          set v1 = (vs1 /. n);

          

           A22: (q . n) = (c1 . n) by A21, FINSEQ_1:def 7;

          

           A23: 1 <= n by A21, FINSEQ_3: 25;

          

           A24: n <= ( len c1) by A21, FINSEQ_3: 25;

          then

           A25: (n + 1) <= ( len vs1) by A1, XREAL_1: 6;

          then

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

          

           A27: n <= ( len vs1) by A16, A24, NAT_1: 12;

          then

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

          

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

          

           A30: (p . n) = (vs1 . n) by A23, A27, FINSEQ_6: 140;

          (c1 . n) joins (v1,v2) by A1, A23, A24;

          hence ex v1,v2 be Element of G st v1 = (p . n) & v2 = (p . (n + 1)) & (q . n) joins (v1,v2) by A22, A28, A26, A30, A29;

        end;

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

          then

          consider k be Nat such that

           A31: k in ( dom c2) and

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

          

           A33: (q . n) = (c2 . k) by A31, A32, FINSEQ_1:def 7;

          

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

          

           A35: 1 <= k by A31, FINSEQ_3: 25;

          

           A36: k <= ( len c2) by A31, FINSEQ_3: 25;

          then

           A37: k <= ( len vs2) by A4, NAT_1: 12;

          reconsider k as Element of NAT by A31;

          

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

          

           A39: (vs2 /. (k + 1)) = (vs2 . (k + 1)) by A4, A36, A34, FINSEQ_4: 15, XREAL_1: 7;

          

           A40: k < ( len vs2) by A4, A36, NAT_1: 13;

          k <= ( len vs2) by A4, A36, NAT_1: 12;

          then

          consider j such that 0 <= j and

           A41: j < ( len vs2) and

           A42: k = (j + 1) by A38, FINSEQ_6: 127;

          

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

          proof

            per cases by A35, XXREAL_0: 1;

              suppose

               A44: 1 = k;

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

              hence thesis by A3, A16, A32, A44, FINSEQ_6: 140;

            end;

              suppose 1 < k;

              then

               A45: 1 <= j by A42, NAT_1: 13;

              

              thus (p . n) = (p . (( len vs1) + j)) by A16, A32, A42

              .= (vs2 . k) by A41, A42, A45, FINSEQ_6: 141;

            end;

          end;

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

          set v1 = (vs2 /. k);

          

           A46: (c2 . k) joins (v1,v2) by A2, A35, A36;

          

           A47: (vs2 /. k) = (vs2 . k) by A35, A37, FINSEQ_4: 15;

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

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

          hence ex v1,v2 be Element of G st v1 = (p . n) & v2 = (p . (n + 1)) & (q . n) joins (v1,v2) by A33, A47, A39, A46, A43;

        end;

      end;

      

       A48: ( len p) = ((( len c1) + ( len c2)) + 1) by A16, A4, A5

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

      thus (c1 ^ c2) is Chain of G

      proof

        hereby

          let n be Nat;

          assume that

           A49: 1 <= n and

           A50: n <= ( len q);

          

           A51: n in ( dom q) by A49, A50, FINSEQ_3: 25;

          per cases by A51, FINSEQ_1: 25;

            suppose

             A52: n in ( dom c1);

            then

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

            

             A54: n <= ( len c1) by A52, FINSEQ_3: 25;

            1 <= n by A52, FINSEQ_3: 25;

            hence ((c1 ^ c2) . n) in the carrier' of G by A54, A53, GRAPH_1:def 14;

          end;

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

            then

            consider k be Nat such that

             A55: k in ( dom c2) and

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

            

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

            

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

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

            hence ((c1 ^ c2) . n) in the carrier' of G by A57, A58, GRAPH_1:def 14;

          end;

        end;

        thus thesis by A48, A6, A17;

      end;

    end;

    theorem :: GRAPH_2:44

    

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

    proof

      assume that

       A1: vs1 is_vertex_seq_of c1 and

       A2: vs2 is_vertex_seq_of c2 and

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

      set p = (vs1 ^' vs2);

      set q = (c1 ^ c2);

      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 vs2 <> {} ;

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

      

      then

       A8: ( 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

         A9: 1 <= n and

         A10: n <= ( len q);

        

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

        n <= ( len p) by A8, A10, NAT_1: 12;

        then

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

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

        then

         A13: (p /. (n + 1)) = (p . (n + 1)) by A8, A10, FINSEQ_4: 15, XREAL_1: 7;

        per cases by A11, FINSEQ_1: 25;

          suppose

           A14: n in ( dom c1);

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

          set v1 = (vs1 /. n);

          

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

          

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

          then

           A17: (n + 1) <= ( len vs1) by A1, XREAL_1: 6;

          then

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

          

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

          then

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

          

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

          

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

          (c1 . n) joins (v1,v2) by A1, A15, A16;

          hence (q . n) joins ((p /. n),(p /. (n + 1))) by A12, A13, A14, A20, A18, A22, A21, FINSEQ_1:def 7;

        end;

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

          then

          consider k be Element of NAT such that

           A23: k in ( dom c2) and

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

          

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

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

          set v1 = (vs2 /. k);

          

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

          then

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

          

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

          then

           A29: (c2 . k) joins (v1,v2) by A2, A26;

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

          then

          consider j such that 0 <= j and

           A30: j < ( len vs2) and

           A31: k = (j + 1) by A25, FINSEQ_6: 127;

          

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

          proof

            per cases by A28, XXREAL_0: 1;

              suppose

               A33: 1 = k;

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

              hence thesis by A3, A6, A24, A33, FINSEQ_6: 140;

            end;

              suppose 1 < k;

              then

               A34: 1 <= j by A31, NAT_1: 13;

              

              thus (p . n) = (p . (( len vs1) + j)) by A6, A24, A31

              .= (vs2 . k) by A30, A31, A34, FINSEQ_6: 141;

            end;

          end;

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

          then

           A35: (vs2 /. (k + 1)) = (vs2 . (k + 1)) by A7, A26, FINSEQ_4: 15, XREAL_1: 7;

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

          then

           A36: (vs2 /. k) = (vs2 . k) by A28, FINSEQ_4: 15;

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

          .= (vs2 . (k + 1)) by A6, A28, A27, FINSEQ_6: 141;

          hence (q . n) joins ((p /. n),(p /. (n + 1))) by A12, A13, A23, A24, A36, A35, A29, A32, FINSEQ_1:def 7;

        end;

      end;

      hence thesis by A4, A5, A8;

    end;

    begin

    

     Lm8: <*v*> is_vertex_seq_of {} by FINSEQ_1: 39;

    definition

      let G;

      let IT be Chain of G;

      :: GRAPH_2:def5

      attr IT is simple means

      : Def9: ex vs st vs is_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 Chain of G;

      existence

      proof

        set x = the Element of G;

        set q = the empty Chain of G;

        take q;

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

        take p;

        thus p is_vertex_seq_of q by Lm8;

        let n, m;

        assume that

         A1: 1 <= n and

         A2: n < m and

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

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

        hence thesis by A3, FINSEQ_1: 39;

      end;

    end

    reserve sc for simple Chain of G;

    theorem :: GRAPH_2:45

    (sc | ( Seg n)) is simple Chain of G

    proof

      reconsider q9 = (sc | ( Seg n)) as Chain of G by GRAPH_1: 4;

      consider vs such that

       A1: vs is_vertex_seq_of sc and

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

      reconsider p9 = (vs | ( Seg (n + 1))) as FinSequence of the carrier of G by FINSEQ_1: 18;

      now

        take p9;

        thus p9 is_vertex_seq_of q9 by A1, Th40;

        let k, m;

        assume that

         A3: 1 <= k and

         A4: k < m and

         A5: m <= ( len p9) and

         A6: (p9 . k) = (p9 . m);

        k <= ( len p9) by A4, A5, XXREAL_0: 2;

        then

         A7: (p9 . k) = (vs . k) by A3, FINSEQ_6: 128;

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

        then

         A8: (p9 . m) = (vs . m) by A5, FINSEQ_6: 128;

        

         A9: ( len p9) <= ( len vs) by FINSEQ_6: 128;

        then

         A10: m <= ( len vs) by A5, XXREAL_0: 2;

        hence k = 1 by A2, A3, A4, A6, A7, A8;

        ( len p9) = ( len vs) or ( len p9) < ( len vs) by A9, XXREAL_0: 1;

        hence m = ( len p9) by A2, A3, A4, A5, A6, A7, A8, A10;

      end;

      hence thesis by Def9;

    end;

    theorem :: GRAPH_2:46

    

     Th46: 2 < ( len sc) & vs1 is_vertex_seq_of sc & vs2 is_vertex_seq_of sc implies vs1 = vs2

    proof

      assume that

       A1: 2 < ( len sc) and

       A2: vs1 is_vertex_seq_of sc and

       A3: vs2 is_vertex_seq_of sc;

      

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

      defpred P[ Nat] means $1 in ( dom vs1) & (vs1 . $1) <> (vs2 . $1);

      set TG = the Target of G;

      set SG = the Source of G;

      

       A5: ( Seg ( len vs1)) = ( dom vs1) by FINSEQ_1:def 3;

      

       A6: ( Seg ( len vs2)) = ( dom vs2) by FINSEQ_1:def 3;

      

       A7: ( len vs2) = (( len sc) + 1) by A3;

      assume

       A8: vs1 <> vs2;

      then

       A9: ex j be Nat st P[j] by A4, A7, FINSEQ_2: 9;

      consider k be Nat such that

       A10: P[k] and

       A11: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A9);

      

       A12: 1 <= k by A10, FINSEQ_3: 25;

      per cases by A12, XXREAL_0: 1;

        suppose

         A13: k = 1;

        set v23 = (vs2 /. ((1 + 1) + 1));

        set v22 = (vs2 /. (1 + 1));

        set v21 = (vs2 /. 1);

        set v13 = (vs1 /. ((1 + 1) + 1));

        set v12 = (vs1 /. (1 + 1));

        set v11 = (vs1 /. 1);

        

         A14: ((1 + 1) + 1) <= ( len vs1) by A1, A4, XREAL_1: 6;

        then

         A15: v13 = (vs1 . ((1 + 1) + 1)) by FINSEQ_4: 15;

        

         A16: 1 <= ( len vs1) by A14, XXREAL_0: 2;

        then

         A17: v11 = (vs1 . 1) by FINSEQ_4: 15;

        

         A18: 1 <= ( len sc) by A1, XXREAL_0: 2;

        then

         A19: (sc . 1) joins (v21,v22) by A3;

        (sc . 1) joins (v11,v12) by A2, A18;

        then

         A20: v11 = v21 & v12 = v22 or v11 = v22 & v12 = v21 by A19;

        

         A21: v21 = (vs2 . 1) by A4, A7, A16, FINSEQ_4: 15;

        consider vs such that

         A22: vs is_vertex_seq_of sc and

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

        sc <> {} by A1;

        then

         A24: vs = vs1 or vs = vs2 by A2, A3, A8, A22, Th34;

        

         A25: v23 = (vs2 . ((1 + 1) + 1)) by A4, A7, A14, FINSEQ_4: 15;

        

         A26: (sc . 2) joins (v22,v23) by A1, A3;

        

         A27: (sc . 2) joins (v12,v13) by A1, A2;

        then

         A28: v21 = v23 by A10, A13, A17, A21, A26, A20;

        v11 = v13 by A10, A13, A17, A21, A27, A26, A20;

        then ((1 + 1) + 1) = ( len vs) by A4, A7, A14, A17, A15, A21, A25, A28, A23, A24;

        hence contradiction by A1, A4, A7, A24;

      end;

        suppose 1 < k;

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

        then

        consider k1 be Nat such that

         A29: 1 <= k1 and

         A30: k1 < k and

         A31: k = (k1 + 1) by FINSEQ_6: 127;

        

         A32: k <= ( len vs1) by A10, FINSEQ_3: 25;

        then

         A33: k1 <= ( len vs1) by A30, XXREAL_0: 2;

        then

         A34: k1 in ( dom vs1) by A29, FINSEQ_3: 25;

        

         A35: (vs1 /. k1) = (vs1 . k1) by A29, A33, FINSEQ_4: 15;

        

         A36: (vs2 /. k) = (vs2 . k) by A4, A7, A5, A6, A10, PARTFUN1:def 6;

        

         A37: (vs1 /. k) = (vs1 . k) by A10, PARTFUN1:def 6;

        

         A38: k1 <= ( len sc) by A4, A31, A32, XREAL_1: 6;

        then (sc . k1) joins ((vs1 /. k1),(vs1 /. (k1 + 1))) by A2, A29;

        then

         A39: (SG . (sc . k1)) = (vs1 /. k1) & (TG . (sc . k1)) = (vs1 /. k) or (SG . (sc . k1)) = (vs1 /. k) & (TG . (sc . k1)) = (vs1 /. k1) by A31;

        (sc . k1) joins ((vs2 /. k1),(vs2 /. (k1 + 1))) by A3, A29, A38;

        then

         A40: (SG . (sc . k1)) = (vs2 /. k1) & (TG . (sc . k1)) = (vs2 /. k) or (SG . (sc . k1)) = (vs2 /. k) & (TG . (sc . k1)) = (vs2 /. k1) by A31;

        (vs2 /. k1) = (vs2 . k1) by A4, A7, A29, A33, FINSEQ_4: 15;

        hence contradiction by A10, A11, A30, A34, A35, A37, A36, A39, A40;

      end;

    end;

    theorem :: GRAPH_2:47

    vs is_vertex_seq_of sc implies for n, m st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs)

    proof

      assume

       A1: vs is_vertex_seq_of sc;

      consider vs1 such that

       A2: vs1 is_vertex_seq_of sc and

       A3: for n, m st 1 <= n & n < m & m <= ( len vs1) & (vs1 . n) = (vs1 . m) holds n = 1 & m = ( len vs1) by Def9;

      per cases ;

        suppose

         A4: ( len sc) <= 2;

        thus thesis

        proof

          ( len sc) = 0 or ... or ( len sc) = 2 by A4;

          per cases ;

            suppose

             A5: ( len sc) = 0 ;

            let n, m;

            ( len vs) = ( 0 + 1) by A1, A5;

            hence thesis by XXREAL_0: 2;

          end;

            suppose ( len sc) = 1;

            then

             A6: ( len vs) = (1 + 1) by A1;

            let n, m;

            assume that

             A7: 1 <= n and

             A8: n < m and

             A9: m <= ( len vs) and (vs . n) = (vs . m);

            

             A10: (n + 1) <= m by A8, NAT_1: 13;

            then (n + 1) <= (1 + 1) by A6, A9, XXREAL_0: 2;

            then n <= 1 by XREAL_1: 6;

            then n = 1 by A7, XXREAL_0: 1;

            hence thesis by A6, A9, A10, XXREAL_0: 1;

          end;

            suppose

             A11: ( len sc) = 2;

            set v12 = (vs1 /. (1 + 1));

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

            set v11 = (vs1 /. 1);

            

             A12: (sc . 1) joins (v11,v12) by A2, A11;

            set v1 = (vs /. 1);

            (sc . 1) joins (v1,v2) by A1, A11;

            then

             A13: v1 = v11 & v2 = v12 or v1 = v12 & v2 = v11 by A12;

            

             A14: ( len vs) = ((1 + 1) + 1) by A1, A11;

            then

             A15: v2 = (vs . (1 + 1)) by FINSEQ_4: 15;

            set v3 = (vs /. ((1 + 1) + 1));

            set v13 = (vs1 /. ((1 + 1) + 1));

            

             A16: (sc . 2) joins (v12,v13) by A2, A11;

            (sc . 2) joins (v2,v3) by A1, A11;

            then

             A17: v2 = v12 & v3 = v13 or v2 = v13 & v3 = v12 by A16;

            

             A18: ( len vs1) = ((1 + 1) + 1) by A2, A11;

            then

             A19: v11 = (vs1 . 1) by FINSEQ_4: 15;

            

             A20: v13 = (vs1 . ((1 + 1) + 1)) by A18, FINSEQ_4: 15;

            

             A21: v12 = (vs1 . (1 + 1)) by A18, FINSEQ_4: 15;

            let n, m;

            assume that

             A22: 1 <= n and

             A23: n < m and

             A24: m <= ( len vs) and

             A25: (vs . n) = (vs . m);

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

            then (n + 1) <= ((1 + 1) + 1) by A14, A24, XXREAL_0: 2;

            then

             A26: n <= (1 + 1) by XREAL_1: 6;

            

             A27: v3 = (vs . ((1 + 1) + 1)) by A14, FINSEQ_4: 15;

            

             A28: v1 = (vs . 1) by A14, FINSEQ_4: 15;

            thus thesis

            proof

              per cases by A22, A26, NAT_1: 9;

                suppose

                 A29: n = 1;

                1 < m by A22, A23, XXREAL_0: 2;

                then

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

                thus thesis

                proof

                  per cases by A14, A24, A30, NAT_1: 9;

                    suppose m = (1 + 1);

                    hence thesis by A3, A18, A28, A15, A19, A21, A13, A25, A29;

                  end;

                    suppose m = ((1 + 1) + 1);

                    hence thesis by A1, A11, A29;

                  end;

                end;

              end;

                suppose

                 A31: n = (1 + 1);

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

                then m = ((1 + 1) + 1) by A14, A24, XXREAL_0: 1;

                hence thesis by A3, A18, A15, A27, A21, A20, A17, A25, A31;

              end;

            end;

          end;

        end;

      end;

        suppose 2 < ( len sc);

        then vs = vs1 by A1, A2, Th46;

        hence thesis by A3;

      end;

    end;

    theorem :: GRAPH_2:48

    

     Th48: not c is simple Chain of G & vs is_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_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 Chain of G and

       A2: vs is_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, Def9;

      

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

      

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

      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;

      then

       A12: (n1 + 1) = n;

      per cases by A7;

        suppose

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

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

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

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

        reconsider p2 = ((m,(( len c) + 1)) -cut vs) as FinSequence of the carrier of G;

        reconsider pp = ((1,n) -cut vs) as FinSequence of the carrier of G;

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

        

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

        

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

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

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

        then

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

        

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

        then

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

        then

        reconsider c2 = ((m,( len c)) -cut c) as Chain of G by A15, Th41;

        

         A18: (( len c2) + m) = (( len c) + 1) by A15, A17, FINSEQ_6:def 4;

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

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

        consider fc be Function such that

         A19: ( dom fc) = domfc and

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

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

        then

         A21: (n - 1) < ((( len c) + 1) - 1) by A9, XREAL_1: 9;

        domfc c= ( Seg ( len c))

        proof

          let x be object;

          assume x in domfc;

          then

          consider kk be Nat such that

           A22: x = kk and

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

          

           A24: 1 <= kk by A15, A23, XXREAL_0: 2;

          kk <= ( len c) by A11, A21, A23, XXREAL_0: 2;

          hence thesis by A22, A24;

        end;

        then

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

        

         A25: fc c= c

        proof

          let p be object;

          assume

           A26: p in fc;

          then

          consider x,y be object such that

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

          

           A28: x in ( dom fc) by A26, A27, FUNCT_1: 1;

          then

          consider kk be Nat such that

           A29: x = kk and

           A30: 1 <= kk & kk <= n1 or m <= kk & kk <= ( len c) by A19;

          

           A31: 1 <= kk by A15, A30, XXREAL_0: 2;

          kk <= ( len c) by A11, A21, A30, XXREAL_0: 2;

          then

           A32: x in ( dom c) by A29, A31, FINSEQ_3: 25;

          y = (fc . x) by A26, A27, FUNCT_1: 1;

          then y = (c . kk) by A19, A20, A28, A29;

          hence thesis by A27, A29, A32, FUNCT_1: 1;

        end;

        1 < n by A3, A13, XXREAL_0: 1;

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

        then

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

        then

        reconsider c1 = ((1,n1) -cut c) as Chain of G by A11, A21, Th41;

        reconsider fc as Subset of c by A25;

        take fc;

        

         A34: pp is_vertex_seq_of c1 by A2, A12, A33, A21, Th42;

        then

         A35: ( len pp) = (( len c1) + 1);

        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

           A36: x in (DL \/ DR);

          per cases by A36, 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

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

        

         A38: 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

             A39: x = k and

             A40: 1 <= k and

             A41: k <= n1;

            k <= ( len c) by A11, A21, A41, XXREAL_0: 2;

            hence x in ( Seg ( len c)) by A39, A40;

          end;

          let x be object;

          assume x in DR;

          then

          consider k be Nat such that

           A42: x = k and

           A43: m <= k and

           A44: k <= ( len c);

          1 <= k by A15, A43, XXREAL_0: 2;

          hence thesis by A42, A44;

        end;

        then

        reconsider DR as finite set;

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

        then

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

        reconsider DL as finite set by A38;

        set SL = ( Sgm DL);

        

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

        set SR = ( Sgm DR);

        

         A47: ( len ( Sgm DR)) = ( card DR) by A38, FINSEQ_3: 39;

        

         A48: m <= ( len c) by A9, A16, NAT_1: 13;

        then

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

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

        then

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

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

        then

         A50: ( - (m - n)) < 0 by A8;

        

         A51: m = (m1 + 1);

        then m1 <= m by NAT_1: 12;

        then

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

        

         A53: p2 is_vertex_seq_of c2 by A2, A15, A17, Th42;

        then

         A54: ( len p2) = (( len c2) + 1);

        then 1 <= ( len p2) by 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 ;

        ( 0 + 1) = 1;

        then

         A55: 1 <= ( len p2) by A54, NAT_1: 13;

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

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

        then

         A56: 1 < ( len p2) by A54, A18, NAT_1: 13;

        (lp21 -' 1) = (lp21 - 1) by A54, A18, A49, XREAL_0:def 2;

        then

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

        

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

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

        

        then

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

        .= ( len c2);

        

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

        now

          let p be object;

          hereby

            assume

             A60: p in c2;

            then

            consider x,y be object such that

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

            

             A62: y = (c2 . x) by A60, A61, FUNCT_1: 1;

            

             A63: x in ( dom c2) by A60, A61, FUNCT_1: 1;

            then

            reconsider k = x as Element of NAT ;

            

             A64: k <= ( len c2) by A63, FINSEQ_3: 25;

            1 <= k by A63, FINSEQ_3: 25;

            then

             A65: (m1 + k) = (SR . k) by A51, A18, A59, A64, FINSEQ_6: 131;

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

            then

            consider i be Nat such that 0 <= i and

             A66: i < ( len c2) and

             A67: k = (i + 1) by A64, FINSEQ_6: 127;

            

             A68: x in ( dom SR) by A58, A47, A63, FINSEQ_3: 29;

            then

             A69: (SR . k) in ( rng SR) by FUNCT_1:def 3;

            then

             A70: x in ( dom (fc * SR)) by A45, A68, FUNCT_1: 11;

            

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

            .= (c . (m + i)) by A45, A65, A69, A67, GRFUNC_1: 2

            .= y by A15, A17, A62, A66, A67, FINSEQ_6:def 4;

            hence p in (fc * ( Sgm DR)) by A61, A70, FUNCT_1: 1;

          end;

          assume

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

          then

          consider x,y be object such that

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

          

           A73: y = ((fc * SR) . x) by A71, A72, FUNCT_1: 1;

          

           A74: x in ( dom (fc * SR)) by A71, A72, FUNCT_1: 1;

          then

           A75: x in ( dom SR) by FUNCT_1: 11;

          then

          reconsider k = x as Element of NAT ;

          

           A76: k <= ( len c2) by A58, A47, A75, FINSEQ_3: 25;

          1 <= k by A75, FINSEQ_3: 25;

          then

           A77: (m1 + k) = (SR . k) by A51, A18, A59, A76, FINSEQ_6: 131;

          

           A78: k in ( dom c2) by A58, A47, A75, FINSEQ_3: 29;

          

           A79: (SR . x) in ( dom fc) by A74, FUNCT_1: 11;

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

          then

          consider i be Nat such that 0 <= i and

           A80: i < ( len c2) and

           A81: k = (i + 1) by A76, FINSEQ_6: 127;

          (c2 . k) = (c . ((m1 + 1) + i)) by A15, A17, A80, A81, FINSEQ_6:def 4

          .= (fc . (SR . k)) by A79, A77, A81, GRFUNC_1: 2

          .= y by A73, A75, FUNCT_1: 13;

          hence p in c2 by A72, A78, FUNCT_1: 1;

        end;

        then

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

        now

          let i, j;

          assume i in DL;

          then

          consider k be Nat such that

           A83: k = i and 1 <= k and

           A84: k <= n1;

          assume j in DR;

          then

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

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

          then k < m by A84, XXREAL_0: 2;

          hence i < j by A83, A85, XXREAL_0: 2;

        end;

        then

         A86: ( Sgm (DL \/ DR)) = (( Sgm DL) ^ ( Sgm DR)) by A38, FINSEQ_3: 42;

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

        

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

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

        consider fvs be Function such that

         A88: ( dom fvs) = domfvs and

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

        

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

        domfvs c= ( Seg ( len vs))

        proof

          let x be object;

          assume x in domfvs;

          then

          consider kk be Nat such that

           A91: x = kk and

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

          

           A93: kk <= ( len vs) by A90, A92, XXREAL_0: 2;

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

          then 1 <= kk by A92, XXREAL_0: 2;

          hence thesis by A91, A93;

        end;

        then

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

        fvs c= vs

        proof

          let p be object;

          assume

           A94: p in fvs;

          then

          consider x,y be object such that

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

          

           A96: x in ( dom fvs) by A94, A95, FUNCT_1: 1;

          then

          consider kk be Nat such that

           A97: x = kk and

           A98: 1 <= kk & kk <= n or (m + 1) <= kk & kk <= ( len vs) by A88;

          

           A99: kk <= ( len vs) by A90, A98, XXREAL_0: 2;

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

          then 1 <= kk by A98, XXREAL_0: 2;

          then

           A100: x in ( dom vs) by A97, A99, FINSEQ_3: 25;

          y = (fvs . x) by A94, A95, FUNCT_1: 1;

          then y = (vs . kk) by A88, A89, A96, A97;

          hence thesis by A95, A97, A100, FUNCT_1: 1;

        end;

        then

        reconsider fvs as Subset of vs;

        

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

        

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

        then

         A103: (p2 . 1) = (vs . m) by A46, A101, FINSEQ_6: 138;

        

         A104: (pp . ( len pp)) = (vs . n) by A3, A90, FINSEQ_6: 138;

        then

        reconsider c9 = (c1 ^ c2) as Chain of G by A6, A34, A53, A103, Th43;

        take fvs;

        take c9;

        take p1 = (pp ^' p2);

        

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

        then

         A106: (( len c1) + 1) = (n1 + 1) by A11, A21, Lm2;

        then ( len c1) = (n - 1) by A10, XREAL_0:def 2;

        

        then ( len c9) = ((n + ( - 1)) + (( len c) + (( - m) + 1))) by A18, FINSEQ_1: 22

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

        hence

         A107: ( len c9) < ( len c) by A50, XREAL_1: 30;

        

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

        then

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

        now

          let p be object;

          hereby

            assume

             A110: p in c1;

            then

            consider x,y be object such that

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

            

             A112: y = (c1 . x) by A110, A111, FUNCT_1: 1;

            

             A113: x in ( dom c1) by A110, A111, FUNCT_1: 1;

            then

            reconsider k = x as Element of NAT ;

            

             A114: k <= ( len c1) by A113, FINSEQ_3: 25;

            

             A115: 1 <= k by A113, FINSEQ_3: 25;

            then

             A116: k in domfc by A106, A114;

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

            then

            consider i be Nat such that 0 <= i and

             A117: i < n1 and

             A118: k = (i + 1) by A106, A114, FINSEQ_6: 127;

            

             A119: x in ( dom SL) by A106, A109, A115, A114;

            then

             A120: k = (SL . k) by A108, FUNCT_1: 18;

            then

             A121: x in ( dom (fc * SL)) by A19, A119, A116, FUNCT_1: 11;

            

            then ((fc * SL) . x) = (fc . k) by A120, FUNCT_1: 12

            .= (c . (1 + i)) by A19, A116, A118, GRFUNC_1: 2

            .= y by A11, A21, A105, A106, A112, A117, A118, Lm2;

            hence p in (fc * ( Sgm DL)) by A111, A121, FUNCT_1: 1;

          end;

          assume

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

          then

          consider x,y be object such that

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

          

           A124: y = ((fc * SL) . x) by A122, A123, FUNCT_1: 1;

          

           A125: x in ( dom (fc * SL)) by A122, A123, FUNCT_1: 1;

          then

           A126: ((fc * SL) . x) = (fc . (SL . x)) by FUNCT_1: 12;

          

           A127: x in ( dom SL) by A125, FUNCT_1: 11;

          then

          consider k be Nat such that

           A128: k = x and

           A129: 1 <= k and

           A130: k <= n1 by A109;

          

           A131: k in ( dom fc) by A19, A129, A130;

          

           A132: k in ( dom c1) by A106, A129, A130, FINSEQ_3: 25;

          

           A133: k = (SL . k) by A108, A127, A128, FUNCT_1: 18;

          ( 0 + 1) <= k by A129;

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

          

          then (c1 . k) = (c . k) by A11, A21, A105, A106, Lm2

          .= y by A124, A126, A128, A131, A133, GRFUNC_1: 2;

          hence p in c1 by A123, A128, A132, FUNCT_1: 1;

        end;

        then

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

        thus p1 is_vertex_seq_of c9 by A6, A34, A53, A103, A104, Th44;

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

        hence ( len p1) < ( len vs) by A9, A107, XREAL_1: 6;

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

        then 1 <= ( len pp) by A34;

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

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

        (p2 . ( len p2)) = (vs . (( len c) + 1)) by A46, A102, A101, FINSEQ_6: 138;

        hence (vs . ( len vs)) = (p1 . ( len p1)) by A9, A56, FINSEQ_6: 142;

        

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

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

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

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

        hence ( Seq fc) = c9 by A19, A37, A86, A45, A134, A82, FINSEQ_6: 150;

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

        

         A136: 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

             A137: x = k and

             A138: 1 <= k and

             A139: k <= n;

            k <= ( len vs) by A90, A139, XXREAL_0: 2;

            hence x in ( Seg ( len vs)) by A137, A138;

          end;

          let x be object;

          assume x in DR;

          then

          consider k be Nat such that

           A140: x = k and

           A141: (m + 1) <= k and

           A142: k <= ( len vs);

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

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

          hence thesis by A140, A142;

        end;

        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

           A143: x in (DL \/ DR);

          per cases by A143, 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

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

        reconsider DR as finite set by A136;

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

        then

         A145: ( rng ( Sgm DR)) c= ( dom fvs) by A88, A144, XBOOLE_1: 7;

        reconsider DL as finite set by A136;

        

         A146: (m + 1) <= ((( len c) + 1) + 1) by A5, A9, XREAL_1: 6;

        

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

        

        then

         A148: (( len p2) + m) = ((( len c) + 1) + 1) by A9, A15, Lm2

        .= (( len p29) + (m + 1)) by A9, A14, A146, Lm2

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

        set SL = ( Sgm DL);

        

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

        then

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

        now

          let p be object;

          hereby

            assume

             A151: p in pp;

            then

            consider x,y be object such that

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

            

             A153: y = (pp . x) by A151, A152, FUNCT_1: 1;

            

             A154: x in ( dom pp) by A151, A152, FUNCT_1: 1;

            then

            reconsider k = x as Element of NAT ;

            

             A155: k <= ( len pp) by A154, FINSEQ_3: 25;

            

             A156: 1 <= k by A154, FINSEQ_3: 25;

            then

             A157: k in domfvs by A11, A35, A106, A155;

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

            then

            consider i be Nat such that 0 <= i and

             A158: i < n and

             A159: k = (i + 1) by A11, A35, A106, A155, FINSEQ_6: 127;

            

             A160: x in ( dom SL) by A11, A35, A106, A150, A156, A155;

            then

             A161: k = (SL . k) by A149, FUNCT_1: 18;

            then

             A162: x in ( dom (fvs * SL)) by A88, A160, A157, FUNCT_1: 11;

            

            then ((fvs * SL) . x) = (fvs . k) by A161, FUNCT_1: 12

            .= (vs . (1 + i)) by A88, A157, A159, GRFUNC_1: 2

            .= y by A3, A11, A90, A35, A106, A153, A158, A159, FINSEQ_6:def 4;

            hence p in (fvs * ( Sgm DL)) by A152, A162, FUNCT_1: 1;

          end;

          assume

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

          then

          consider x,y be object such that

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

          

           A165: y = ((fvs * SL) . x) by A163, A164, FUNCT_1: 1;

          

           A166: x in ( dom (fvs * SL)) by A163, A164, FUNCT_1: 1;

          then

           A167: ((fvs * SL) . x) = (fvs . (SL . x)) by FUNCT_1: 12;

          

           A168: x in ( dom SL) by A166, FUNCT_1: 11;

          then

          consider k be Nat such that

           A169: k = x and

           A170: 1 <= k and

           A171: k <= n by A150;

          

           A172: k in ( dom fvs) by A88, A170, A171;

          

           A173: k = (SL . k) by A149, A168, A169, FUNCT_1: 18;

          

           A174: k in ( dom pp) by A11, A35, A106, A170, A171, FINSEQ_3: 25;

          ( 0 + 1) <= k by A170;

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

          

          then (pp . k) = (vs . k) by A3, A11, A90, A35, A106, FINSEQ_6:def 4

          .= y by A165, A167, A169, A172, A173, GRFUNC_1: 2;

          hence p in pp by A164, A169, A174, FUNCT_1: 1;

        end;

        then

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

        set SR = ( Sgm DR);

        

         A176: ( len ( Sgm DR)) = ( card DR) by A136, FINSEQ_3: 39;

        

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

        .= (m + ((((( len c) - m) + 1) + 1) - 1)) by A53, A18

        .= (( len c) + 1);

        

        then

         A178: ( card DR) = ((lp21 - 1) + 1) by A9, FINSEQ_6: 130

        .= lp21;

        

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

        now

          let p be object;

          hereby

            assume

             A180: p in p29;

            then

            consider x,y be object such that

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

            

             A182: y = (p29 . x) by A180, A181, FUNCT_1: 1;

            

             A183: x in ( dom p29) by A180, A181, FUNCT_1: 1;

            then

            reconsider k = x as Element of NAT ;

            

             A184: k <= ( len p29) by A183, FINSEQ_3: 25;

            1 <= k by A183, FINSEQ_3: 25;

            then

             A185: (m + k) = (SR . k) by A9, A177, A148, A57, A184, FINSEQ_6: 131;

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

            then

            consider i be Nat such that 0 <= i and

             A186: i < ( len p29) and

             A187: k = (i + 1) by A184, FINSEQ_6: 127;

            

             A188: x in ( dom SR) by A178, A148, A176, A183, FINSEQ_3: 29;

            then

             A189: (SR . k) in ( rng SR) by FUNCT_1:def 3;

            then

             A190: x in ( dom (fvs * SR)) by A145, A188, FUNCT_1: 11;

            

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

            .= (vs . ((m + 1) + i)) by A145, A185, A189, A187, GRFUNC_1: 2

            .= y by A9, A87, A179, A182, A186, A187, Lm2;

            hence p in (fvs * ( Sgm DR)) by A181, A190, FUNCT_1: 1;

          end;

          assume

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

          then

          consider x,y be object such that

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

          

           A193: y = ((fvs * SR) . x) by A191, A192, FUNCT_1: 1;

          

           A194: x in ( dom (fvs * SR)) by A191, A192, FUNCT_1: 1;

          then

           A195: x in ( dom SR) by FUNCT_1: 11;

          then

          reconsider k = x as Element of NAT ;

          

           A196: k <= ( len p29) by A178, A148, A176, A195, FINSEQ_3: 25;

          1 <= k by A195, FINSEQ_3: 25;

          then

           A197: (m + k) = (SR . k) by A9, A177, A148, A57, A196, FINSEQ_6: 131;

          

           A198: k in ( dom p29) by A178, A148, A176, A195, FINSEQ_3: 29;

          

           A199: (SR . x) in ( dom fvs) by A194, FUNCT_1: 11;

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

          then

          consider i be Nat such that 0 <= i and

           A200: i < ( len p29) and

           A201: k = (i + 1) by A196, FINSEQ_6: 127;

          (p29 . k) = (vs . ((m + 1) + i)) by A9, A87, A179, A200, A201, Lm2

          .= (fvs . (SR . k)) by A199, A197, A201, GRFUNC_1: 2

          .= y by A193, A195, FUNCT_1: 13;

          hence p in p29 by A192, A198, FUNCT_1: 1;

        end;

        then

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

        now

          let i, j;

          assume i in DL;

          then

          consider k be Nat such that

           A203: k = i and 1 <= k and

           A204: k <= n;

          

           A205: k < m by A4, A204, XXREAL_0: 2;

          assume j in DR;

          then

          consider l be Nat such that

           A206: l = j and

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

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

          then m <= l by A207, XXREAL_0: 2;

          hence i < j by A203, A206, A205, XXREAL_0: 2;

        end;

        then

         A208: ( Sgm (DL \/ DR)) = (( Sgm DL) ^ ( Sgm DR)) by A136, FINSEQ_3: 42;

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

        .= <*(vs . (m + 0 ))*> by A9, A15, A54, A147, Lm2

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

        then

         A209: p1 = (pp ^ p29) by A135, A52, FINSEQ_1: 33;

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

        then ( rng ( Sgm DL)) c= ( dom fvs) by A88, A144, XBOOLE_1: 7;

        hence thesis by A88, A209, A144, A208, A145, A175, A202, FINSEQ_6: 150;

      end;

        suppose

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

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

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

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

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

        consider fc be Function such that

         A211: ( dom fc) = domfc and

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

        

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

        then (1 - 1) < (m - 1) by XREAL_1: 9;

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

        then

         A214: ( - (m - 1)) < 0 ;

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

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

        then

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

        

         A215: m = (m1 + 1);

        domfc c= ( Seg ( len c))

        proof

          let x be object;

          assume x in domfc;

          then

          consider kk be Nat such that

           A216: x = kk and

           A217: m <= kk and

           A218: kk <= ( len c);

          1 <= kk by A213, A217, XXREAL_0: 2;

          hence thesis by A216, A218;

        end;

        then

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

        fc c= c

        proof

          let p be object;

          assume

           A219: p in fc;

          then

          consider x,y be object such that

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

          

           A221: x in ( dom fc) by A219, A220, FUNCT_1: 1;

          then

          consider kk be Nat such that

           A222: x = kk and

           A223: m <= kk and

           A224: kk <= ( len c) by A211;

          1 <= kk by A213, A223, XXREAL_0: 2;

          then

           A225: x in ( dom c) by A222, A224, FINSEQ_3: 25;

          y = (fc . x) by A219, A220, FUNCT_1: 1;

          then y = (c . kk) by A211, A212, A221, A222;

          hence thesis by A220, A222, A225, FUNCT_1: 1;

        end;

        then

        reconsider fc as Subset of c;

        take fc;

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

        consider fvs be Function such that

         A226: ( dom fvs) = domfvs and

         A227: 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

           A228: x = kk and

           A229: m <= kk and

           A230: kk <= ( len vs);

          1 <= kk by A213, A229, XXREAL_0: 2;

          hence thesis by A228, A230;

        end;

        then

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

        

         A231: fvs c= vs

        proof

          let p be object;

          assume

           A232: p in fvs;

          then

          consider x,y be object such that

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

          

           A234: x in ( dom fvs) by A232, A233, FUNCT_1: 1;

          then

          consider kk be Nat such that

           A235: x = kk and

           A236: m <= kk and

           A237: kk <= ( len vs) by A226;

          1 <= kk by A213, A236, XXREAL_0: 2;

          then

           A238: x in ( dom vs) by A235, A237, FINSEQ_3: 25;

          y = (fvs . x) by A232, A233, FUNCT_1: 1;

          then y = (vs . kk) by A226, A227, A234, A235;

          hence thesis by A233, A235, A238, FUNCT_1: 1;

        end;

        

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

        then

         A240: m <= ( len c) by A9, NAT_1: 13;

        then

        reconsider c2 = ((m,( len c)) -cut c) as Chain of G by A213, Th41;

        

         A241: m <= ( len c) by A9, A239, NAT_1: 13;

        reconsider fvs as Subset of vs by A231;

        take fvs;

        take c1 = c2;

        take p1 = p2;

        

         A242: (( len c2) + m) = (( len c) + 1) by A4, A5, A9, A210, Lm2;

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

        hence

         A243: ( len c1) < ( len c) by A214, XREAL_1: 30;

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

        hence p1 is_vertex_seq_of c1 by A2, A241, Th42;

        p2 is_vertex_seq_of c2 by A2, A240, A213, Th42;

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

        hence ( len p1) < ( len vs) by A9, A243, XREAL_1: 6;

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

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

        

         A244: domfvs c= ( Seg ( len vs))

        proof

          let x be object;

          assume x in domfvs;

          then

          consider k be Nat such that

           A245: x = k and

           A246: m <= k and

           A247: k <= ( len vs);

          1 <= k by A213, A246, XXREAL_0: 2;

          hence thesis by A245, A247;

        end;

        

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

        proof

          let x be object;

          assume x in domfc;

          then

          consider k be Nat such that

           A249: x = k and

           A250: m <= k and

           A251: k <= ( len c);

          1 <= k by A213, A250, XXREAL_0: 2;

          hence thesis by A249, A251;

        end;

        then

        reconsider domfc as finite set;

        

         A252: ( len ( Sgm domfc)) = ( card domfc) by A248, FINSEQ_3: 39;

        reconsider domfvs as finite set by A244;

        

         A253: ( rng ( Sgm domfvs)) c= ( dom fvs) by A226, A244, FINSEQ_1:def 13;

        set SR = ( Sgm domfc);

        

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

        

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

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

        then

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

        

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

        (( len c2) -' 1) = (( len c2) - 1) by A242, A255, XREAL_0:def 2;

        then

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

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

        

        then

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

        .= ( len c2);

        

         A258: ( rng ( Sgm domfc)) c= ( dom fc) by A211, A248, FINSEQ_1:def 13;

        now

          let p be object;

          hereby

            assume

             A259: p in c2;

            then

            consider x,y be object such that

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

            

             A261: y = (c2 . x) by A259, A260, FUNCT_1: 1;

            

             A262: x in ( dom c2) by A259, A260, FUNCT_1: 1;

            then

            reconsider k = x as Element of NAT ;

            

             A263: k <= ( len c2) by A262, FINSEQ_3: 25;

            1 <= k by A262, FINSEQ_3: 25;

            then

             A264: (m1 + k) = (SR . k) by A242, A215, A256, A263, FINSEQ_6: 131;

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

            then

            consider i be Nat such that 0 <= i and

             A265: i < ( len c2) and

             A266: k = (i + 1) by A263, FINSEQ_6: 127;

            

             A267: x in ( dom SR) by A257, A252, A262, FINSEQ_3: 29;

            then

             A268: (SR . k) in ( rng SR) by FUNCT_1:def 3;

            then

             A269: x in ( dom (fc * SR)) by A258, A267, FUNCT_1: 11;

            

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

            .= (c . (m + i)) by A258, A264, A268, A266, GRFUNC_1: 2

            .= y by A4, A5, A9, A210, A261, A265, A266, Lm2;

            hence p in (fc * ( Sgm domfc)) by A260, A269, FUNCT_1: 1;

          end;

          assume

           A270: p in (fc * ( Sgm domfc));

          then

          consider x,y be object such that

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

          

           A272: y = ((fc * SR) . x) by A270, A271, FUNCT_1: 1;

          

           A273: x in ( dom (fc * SR)) by A270, A271, FUNCT_1: 1;

          then

           A274: x in ( dom SR) by FUNCT_1: 11;

          then

          reconsider k = x as Element of NAT ;

          

           A275: k <= ( len c2) by A257, A252, A274, FINSEQ_3: 25;

          1 <= k by A274, FINSEQ_3: 25;

          then

           A276: (m1 + k) = (SR . k) by A242, A215, A256, A275, FINSEQ_6: 131;

          

           A277: k in ( dom c2) by A257, A252, A274, FINSEQ_3: 29;

          

           A278: (SR . x) in ( dom fc) by A273, FUNCT_1: 11;

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

          then

          consider i be Nat such that 0 <= i and

           A279: i < ( len c2) and

           A280: k = (i + 1) by A275, FINSEQ_6: 127;

          (c2 . k) = (c . ((m1 + 1) + i)) by A4, A5, A9, A210, A279, A280, Lm2

          .= (fc . (SR . k)) by A278, A276, A280, GRFUNC_1: 2

          .= y by A272, A274, FUNCT_1: 13;

          hence p in c2 by A271, A277, FUNCT_1: 1;

        end;

        hence ( Seq fc) = c1 by A211, TARSKI: 2;

        set SR = ( Sgm domfvs);

        

         A281: ( len ( Sgm domfvs)) = ( card domfvs) by A244, FINSEQ_3: 39;

        

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

        then

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

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

        then 1 <= ( len p2) by A242, 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 ;

        (m + lp21) = (( len c) + 1) by A283;

        

        then

         A284: ( card domfvs) = ((( len p2) + ( - 1)) + 1) by A9, FINSEQ_6: 130

        .= ( len p2);

        

         A285: (m + lp21) = (m1 + ( len p2));

        now

          let p be object;

          hereby

            assume

             A286: p in p2;

            then

            consider x,y be object such that

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

            

             A288: y = (p2 . x) by A286, A287, FUNCT_1: 1;

            

             A289: x in ( dom p2) by A286, A287, FUNCT_1: 1;

            then

            reconsider k = x as Element of NAT ;

            

             A290: k <= ( len p2) by A289, FINSEQ_3: 25;

            1 <= k by A289, FINSEQ_3: 25;

            then

             A291: (m1 + k) = (SR . k) by A9, A215, A283, A285, A290, FINSEQ_6: 131;

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

            then

            consider i be Nat such that 0 <= i and

             A292: i < ( len p2) and

             A293: k = (i + 1) by A290, FINSEQ_6: 127;

            

             A294: x in ( dom SR) by A284, A281, A289, FINSEQ_3: 29;

            then

             A295: (SR . k) in ( rng SR) by FUNCT_1:def 3;

            then

             A296: x in ( dom (fvs * SR)) by A253, A294, FUNCT_1: 11;

            

            then ((fvs * SR) . x) = (fvs . (m1 + k)) by A291, FUNCT_1: 12

            .= (vs . (m + i)) by A253, A291, A295, A293, GRFUNC_1: 2

            .= y by A4, A210, A282, A254, A288, A292, A293, Lm2;

            hence p in (fvs * ( Sgm domfvs)) by A287, A296, FUNCT_1: 1;

          end;

          assume

           A297: p in (fvs * ( Sgm domfvs));

          then

          consider x,y be object such that

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

          

           A299: y = ((fvs * SR) . x) by A297, A298, FUNCT_1: 1;

          

           A300: x in ( dom (fvs * SR)) by A297, A298, FUNCT_1: 1;

          then

           A301: x in ( dom SR) by FUNCT_1: 11;

          then

          reconsider k = x as Element of NAT ;

          

           A302: k <= ( len p2) by A284, A281, A301, FINSEQ_3: 25;

          1 <= k by A301, FINSEQ_3: 25;

          then

           A303: (m1 + k) = (SR . k) by A9, A215, A283, A285, A302, FINSEQ_6: 131;

          

           A304: k in ( dom p2) by A284, A281, A301, FINSEQ_3: 29;

          

           A305: (SR . x) in ( dom fvs) by A300, FUNCT_1: 11;

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

          then

          consider i be Nat such that 0 <= i and

           A306: i < ( len p2) and

           A307: k = (i + 1) by A302, FINSEQ_6: 127;

          (p2 . k) = (vs . ((m1 + 1) + i)) by A4, A210, A282, A254, A306, A307, Lm2

          .= (fvs . (SR . k)) by A305, A303, A307, GRFUNC_1: 2

          .= y by A299, A301, FUNCT_1: 13;

          hence p in p2 by A298, A304, FUNCT_1: 1;

        end;

        hence thesis by A226, TARSKI: 2;

      end;

        suppose

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

        set domfvs = { k where k be Nat : 1 <= k & k <= n };

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

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

        reconsider domfc = { k where k be Nat : 1 <= k & k <= n1 } as set;

        consider fc be Function such that

         A309: ( dom fc) = domfc and

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

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

        then

         A311: (n - 1) < ((( len c) + 1) - 1) by A9, XREAL_1: 9;

        domfc c= ( Seg ( len c))

        proof

          let x be object;

          assume x in domfc;

          then

          consider kk be Nat such that

           A312: x = kk and

           A313: 1 <= kk and

           A314: kk <= n1;

          kk <= ( len c) by A11, A311, A314, XXREAL_0: 2;

          hence thesis by A312, A313;

        end;

        then

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

        1 < n by A3, A308, XXREAL_0: 1;

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

        then

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

        then

        reconsider c1 = ((1,n1) -cut c) as Chain of G by A11, A311, Th41;

        

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

        then

         A317: (( len c1) + 1) = (n1 + 1) by A11, A311, Lm2;

        then

         A318: ( len c1) = (n - 1) by A10, XREAL_0:def 2;

        

         A319: fc c= c

        proof

          let p be object;

          assume

           A320: p in fc;

          then

          consider x,y be object such that

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

          

           A322: x in ( dom fc) by A320, A321, FUNCT_1: 1;

          then

          consider kk be Nat such that

           A323: x = kk and

           A324: 1 <= kk and

           A325: kk <= n1 by A309;

          kk <= ( len c) by A11, A311, A325, XXREAL_0: 2;

          then

           A326: x in ( dom c) by A323, A324, FINSEQ_3: 25;

          y = (fc . x) by A320, A321, FUNCT_1: 1;

          then y = (c . kk) by A309, A310, A322, A323;

          hence thesis by A321, A323, A326, FUNCT_1: 1;

        end;

        

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

        proof

          let x be object;

          assume x in domfc;

          then

          consider k be Nat such that

           A328: x = k and

           A329: 1 <= k and

           A330: k <= n1;

          k <= ( len c) by A11, A311, A330, XXREAL_0: 2;

          hence thesis by A328, A329;

        end;

        reconsider fc as Subset of c by A319;

        take fc;

        reconsider domfc as finite set by A327;

        set SL = ( Sgm domfc);

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

        consider fvs be Function such that

         A331: ( dom fvs) = domfvs and

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

        

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

        domfvs c= ( Seg ( len vs))

        proof

          let x be object;

          assume x in domfvs;

          then

          consider kk be Nat such that

           A334: x = kk and

           A335: 1 <= kk and

           A336: kk <= n;

          kk <= ( len vs) by A333, A336, XXREAL_0: 2;

          hence thesis by A334, A335;

        end;

        then

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

        fvs c= vs

        proof

          let p be object;

          assume

           A337: p in fvs;

          then

          consider x,y be object such that

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

          

           A339: x in ( dom fvs) by A337, A338, FUNCT_1: 1;

          then

          consider kk be Nat such that

           A340: x = kk and

           A341: 1 <= kk and

           A342: kk <= n by A331;

          kk <= ( len vs) by A333, A342, XXREAL_0: 2;

          then

           A343: x in ( dom vs) by A340, A341, FINSEQ_3: 25;

          y = (fvs . x) by A337, A338, FUNCT_1: 1;

          then y = (vs . kk) by A331, A332, A339, A340;

          hence thesis by A338, A340, A343, FUNCT_1: 1;

        end;

        then

        reconsider fvs as Subset of vs;

        domfvs c= ( Seg ( len vs))

        proof

          let x be object;

          assume x in domfvs;

          then

          consider k be Nat such that

           A344: x = k and

           A345: 1 <= k and

           A346: k <= n;

          k <= ( len vs) by A333, A346, XXREAL_0: 2;

          hence thesis by A344, A345;

        end;

        then

        reconsider domfvs as finite set;

        take fvs;

        take c9 = c1;

        take p1 = pp;

        

         A347: pp is_vertex_seq_of c1 by A2, A12, A315, A311, Th42;

        then

         A348: ( len pp) = (( len c1) + 1);

        thus ( len c9) < ( len c) by A10, A311, A317, XREAL_0:def 2;

        thus p1 is_vertex_seq_of c9 by A2, A12, A315, A311, Th42;

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

        hence ( len p1) < ( len vs) by A4, A5, A318, XXREAL_0: 2;

        thus (vs . 1) = (p1 . 1) by A3, A333, FINSEQ_6: 138;

        thus (vs . ( len vs)) = (p1 . ( len p1)) by A3, A4, A6, A308, FINSEQ_6: 138;

        

         A349: ( Sgm domfc) = ( idseq n1) by FINSEQ_3: 48;

        then

         A350: ( dom ( Sgm domfc)) = ( Seg n1);

        now

          let p be object;

          hereby

            assume

             A351: p in c1;

            then

            consider x,y be object such that

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

            

             A353: y = (c1 . x) by A351, A352, FUNCT_1: 1;

            

             A354: x in ( dom c1) by A351, A352, FUNCT_1: 1;

            then

            reconsider k = x as Element of NAT ;

            

             A355: k <= ( len c1) by A354, FINSEQ_3: 25;

            

             A356: 1 <= k by A354, FINSEQ_3: 25;

            then x in ( dom SL) by A317, A350, A355;

            then

             A357: k = (SL . k) by A349, FUNCT_1: 18;

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

            then

            consider i be Nat such that 0 <= i and

             A358: i < n1 and

             A359: k = (i + 1) by A317, A355, FINSEQ_6: 127;

            

             A360: k in domfc by A317, A356, A355;

            then

             A361: x in ( dom (fc * SL)) by A309, A350, A357, FUNCT_1: 11;

            

            then ((fc * SL) . x) = (fc . k) by A357, FUNCT_1: 12

            .= (c . (1 + i)) by A309, A360, A359, GRFUNC_1: 2

            .= y by A11, A311, A316, A317, A353, A358, A359, Lm2;

            hence p in (fc * ( Sgm domfc)) by A352, A361, FUNCT_1: 1;

          end;

          assume

           A362: p in (fc * ( Sgm domfc));

          then

          consider x,y be object such that

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

          

           A364: y = ((fc * SL) . x) by A362, A363, FUNCT_1: 1;

          

           A365: x in ( dom (fc * SL)) by A362, A363, FUNCT_1: 1;

          then

           A366: ((fc * SL) . x) = (fc . (SL . x)) by FUNCT_1: 12;

          

           A367: x in ( dom SL) by A365, FUNCT_1: 11;

          then

          consider k be Nat such that

           A368: k = x and

           A369: 1 <= k and

           A370: k <= n1 by A350;

          

           A371: k in ( dom fc) by A309, A369, A370;

          

           A372: k in ( dom c1) by A317, A369, A370, FINSEQ_3: 25;

          

           A373: k = (SL . k) by A349, A367, A368, FUNCT_1: 18;

          ( 0 + 1) <= k by A369;

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

          

          then (c1 . k) = (c . k) by A11, A311, A316, A317, Lm2

          .= y by A364, A366, A368, A371, A373, GRFUNC_1: 2;

          hence p in c1 by A363, A368, A372, FUNCT_1: 1;

        end;

        hence ( Seq fc) = c9 by A309, TARSKI: 2;

        set SL = ( Sgm domfvs);

        

         A374: ( Sgm domfvs) = ( idseq n) by FINSEQ_3: 48;

        then

         A375: ( dom ( Sgm domfvs)) = ( Seg n);

        now

          let p be object;

          hereby

            assume

             A376: p in pp;

            then

            consider x,y be object such that

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

            

             A378: y = (pp . x) by A376, A377, FUNCT_1: 1;

            

             A379: x in ( dom pp) by A376, A377, FUNCT_1: 1;

            then

            reconsider k = x as Element of NAT ;

            

             A380: k <= ( len pp) by A379, FINSEQ_3: 25;

            

             A381: 1 <= k by A379, FINSEQ_3: 25;

            then x in ( dom SL) by A348, A318, A375, A380;

            then

             A382: k = (SL . k) by A374, FUNCT_1: 18;

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

            then

            consider i be Nat such that 0 <= i and

             A383: i < n and

             A384: k = (i + 1) by A348, A318, A380, FINSEQ_6: 127;

            

             A385: k in domfvs by A348, A318, A381, A380;

            then

             A386: x in ( dom (fvs * SL)) by A331, A375, A382, FUNCT_1: 11;

            

            then ((fvs * SL) . x) = (fvs . k) by A382, FUNCT_1: 12

            .= (vs . (1 + i)) by A331, A385, A384, GRFUNC_1: 2

            .= y by A3, A333, A348, A318, A378, A383, A384, FINSEQ_6:def 4;

            hence p in (fvs * ( Sgm domfvs)) by A377, A386, FUNCT_1: 1;

          end;

          assume

           A387: p in (fvs * ( Sgm domfvs));

          then

          consider x,y be object such that

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

          

           A389: y = ((fvs * SL) . x) by A387, A388, FUNCT_1: 1;

          

           A390: x in ( dom (fvs * SL)) by A387, A388, FUNCT_1: 1;

          then

           A391: ((fvs * SL) . x) = (fvs . (SL . x)) by FUNCT_1: 12;

          

           A392: x in ( dom SL) by A390, FUNCT_1: 11;

          then

          consider k be Nat such that

           A393: k = x and

           A394: 1 <= k and

           A395: k <= n by A375;

          

           A396: k in ( dom fvs) by A331, A394, A395;

          

           A397: k in ( dom pp) by A348, A318, A394, A395, FINSEQ_3: 25;

          

           A398: k = (SL . k) by A374, A392, A393, FUNCT_1: 18;

          ( 0 + 1) <= k by A394;

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

          

          then (pp . k) = (vs . k) by A3, A333, A348, A318, FINSEQ_6:def 4

          .= y by A389, A391, A393, A396, A398, GRFUNC_1: 2;

          hence p in pp by A388, A393, A397, FUNCT_1: 1;

        end;

        hence thesis by A331, TARSKI: 2;

      end;

    end;

    theorem :: GRAPH_2:49

    vs is_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_vertex_seq_of sc & (vs . 1) = (vs1 . 1) & (vs . ( len vs)) = (vs1 . ( len vs1))

    proof

      assume

       A1: vs is_vertex_seq_of c;

      per cases ;

        suppose c is simple Chain of G;

        then

        reconsider sc = c as simple Chain of G;

        reconsider fvs = vs as Subset of vs by FINSEQ_6: 152;

        reconsider fc = c as Subset of c by FINSEQ_6: 152;

        take fc, fvs, sc, vs;

        thus ( Seq fc) = sc & ( Seq fvs) = vs by FINSEQ_3: 116;

        thus vs is_vertex_seq_of sc by A1;

        thus thesis;

      end;

        suppose

         A2: not c is simple Chain of G;

        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_vertex_seq_of c1 & (vs . 1) = (vs1 . 1) & (vs . ( len vs)) = (vs1 . ( len vs1)) & ( len c1) = $1 & not c1 is simple Chain of G;

         P[( len c) qua Element of NAT ]

        proof

          reconsider fvs = vs as Subset of vs by FINSEQ_6: 152;

          reconsider fc = c as Subset of c by FINSEQ_6: 152;

          take fc, fvs, c, vs;

          thus ( Seq fc) = c & ( Seq fvs) = vs by FINSEQ_3: 116;

          thus vs is_vertex_seq_of c by A1;

          thus (vs . 1) = (vs . 1) & (vs . ( len vs)) = (vs . ( len vs));

          thus thesis by A2;

        end;

        then

         A3: ex k be Nat st P[k];

        consider k be Nat such that

         A4: P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A3);

        consider fc be Subset of c, fvs be Subset of vs, c1, vs1 such that

         A5: ( Seq fc) = c1 and

         A6: ( Seq fvs) = vs1 and

         A7: vs1 is_vertex_seq_of c1 and

         A8: (vs . 1) = (vs1 . 1) and

         A9: (vs . ( len vs)) = (vs1 . ( len vs1)) and

         A10: ( len c1) = k and

         A11: not c1 is simple Chain of G by A4;

        consider fc1 be Subset of c1, fvs1 be Subset of vs1, c2, vs2 such that

         A12: ( len c2) < ( len c1) and

         A13: vs2 is_vertex_seq_of c2 and ( len vs2) < ( len vs1) and

         A14: (vs1 . 1) = (vs2 . 1) and

         A15: (vs1 . ( len vs1)) = (vs2 . ( len vs2)) and

         A16: ( Seq fc1) = c2 and

         A17: ( Seq fvs1) = vs2 by A7, A11, Th48;

        reconsider fc9 = (fc | ( rng (( Sgm ( dom fc)) | ( dom fc1)))) as Subset of c by FINSEQ_6: 153;

        reconsider fvs9 = (fvs | ( rng (( Sgm ( dom fvs)) | ( dom fvs1)))) as Subset of vs by FINSEQ_6: 153;

        

         A18: ( Seq fvs9) = vs2 by A6, A17, FINSEQ_6: 154;

        

         A19: ( Seq fc9) = c2 by A5, A16, FINSEQ_6: 154;

        then c2 is simple Chain of G implies thesis by A8, A9, A13, A14, A15, A18;

        hence thesis by A4, A8, A9, A10, A12, A13, A14, A15, A19, A18;

      end;

    end;

    registration

      let G;

      cluster empty -> one-to-one for Chain of G;

      correctness ;

    end

    theorem :: GRAPH_2:50

    p is Path of G implies (p | ( Seg n)) is Path of G

    proof

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

      assume

       A1: p is Path of G;

      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;

      hence thesis by A1, GRAPH_1: 4, GRAPH_1:def 16;

    end;

    registration

      let G;

      cluster simple for Path of G;

      existence

      proof

        set x = the Element of G;

        set q = the empty Chain of G;

        reconsider q as one-to-one Chain of G;

        take q;

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

        take p;

        thus p is_vertex_seq_of q by Lm8;

        let n, m;

        assume that

         A1: 1 <= n and

         A2: n < m and

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

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

        hence thesis by A3, FINSEQ_1: 39;

      end;

    end

    theorem :: GRAPH_2:51

    2 < ( len sc) implies sc is Path of G

    proof

      assume

       A1: 2 < ( len sc);

      assume not sc is Path of G;

      then

      consider m, n such that

       A2: 1 <= m and

       A3: m < n and

       A4: n <= ( len sc) and

       A5: (sc . m) = (sc . n) by GRAPH_1:def 16;

      consider vs such that

       A6: vs is_vertex_seq_of sc and

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

      

       A8: ( len vs) = (( len sc) + 1) by A6;

      then

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

      set v29 = (vs /. (n + 1));

      set v19 = (vs /. n);

      

       A10: 1 <= n by A2, A3, XXREAL_0: 2;

      then

       A11: (sc . n) joins (v19,v29) by A4, A6;

      

       A12: n <= ( len vs) by A4, A8, NAT_1: 12;

      then

       A13: v19 = (vs . n) by A10, FINSEQ_4: 15;

      set v1 = (vs /. m);

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

      m <= ( len sc) by A3, A4, XXREAL_0: 2;

      then

       A14: (sc . m) joins (v1,v2) by A2, A6;

      

       A15: (n + 1) <= ( len vs) by A4, A8, XREAL_1: 6;

      then

       A16: v29 = (vs . (n + 1)) by FINSEQ_4: 15, NAT_1: 12;

      

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

      then

       A18: m < (n + 1) by NAT_1: 12;

      then m <= ( len vs) by A15, XXREAL_0: 2;

      then

       A19: v1 = (vs . m) by A2, FINSEQ_4: 15;

      (m + 1) <= ( len vs) by A17, A15, XXREAL_0: 2;

      then

       A20: v2 = (vs . (m + 1)) by FINSEQ_4: 15, NAT_1: 12;

      per cases by A5, A14, A11;

        suppose

         A21: v1 = v19 & v2 = v29;

        then m = 1 by A2, A3, A7, A12, A19, A13;

        hence contradiction by A7, A17, A15, A20, A16, A21;

      end;

        suppose

         A22: v1 = v29 & v2 = v19;

        then

         A23: (n + 1) = ( len vs) by A2, A7, A18, A9, A19, A16;

        m = 1 by A2, A7, A18, A9, A19, A16, A22;

        hence contradiction by A1, A7, A8, A12, A20, A13, A22, A23;

      end;

    end;

    theorem :: GRAPH_2:52

    sc is Path of G iff ( len sc) = 0 or ( len sc) = 1 or (sc . 1) <> (sc . 2)

    proof

      hereby

        assume

         A1: sc is Path of G;

        assume

         A2: not ( len sc) = 0 ;

        assume not ( len sc) = 1;

        then ( len sc) > 1 by A2, NAT_1: 25;

        then

         A3: (1 + 1) <= ( len sc) by NAT_1: 13;

        assume (sc . 1) = (sc . 2);

        hence contradiction by A1, A3, GRAPH_1:def 16;

      end;

      assume

       A4: ( len sc) = 0 or ( len sc) = 1 or (sc . 1) <> (sc . 2);

      per cases by A4;

        suppose ( len sc) = 0 ;

        then for n, m st 1 <= n & n < m & m <= ( len sc) holds (sc . n) <> (sc . m);

        hence thesis by GRAPH_1:def 16;

      end;

        suppose ( len sc) = 1;

        then for n, m st 1 <= n & n < m & m <= ( len sc) holds (sc . n) <> (sc . m) by XXREAL_0: 2;

        hence thesis by GRAPH_1:def 16;

      end;

        suppose

         A5: (sc . 1) <> (sc . 2);

        now

          let n, m;

          assume that

           A6: 1 <= n and

           A7: n < m and

           A8: m <= ( len sc);

          thus (sc . n) <> (sc . m)

          proof

            consider vs such that

             A9: vs is_vertex_seq_of sc and

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

            set vm1 = (vs /. (m + 1));

            

             A11: ( len vs) = (( len sc) + 1) by A9;

            then

             A12: (m + 1) <= ( len vs) by A8, XREAL_1: 6;

            then

             A13: vm1 = (vs . (m + 1)) by FINSEQ_4: 15, NAT_1: 12;

            set vn1 = (vs /. (n + 1));

            set vn = (vs /. n);

            

             A14: n <= ( len sc) by A7, A8, XXREAL_0: 2;

            then

             A15: (sc . n) joins (vn,vn1) by A6, A9;

            (n + 1) <= ( len vs) by A11, A14, XREAL_1: 6;

            then

             A16: vn1 = (vs . (n + 1)) by FINSEQ_4: 15, NAT_1: 12;

            n <= ( len vs) by A11, A14, NAT_1: 12;

            then

             A17: vn = (vs . n) by A6, FINSEQ_4: 15;

            set vm = (vs /. m);

            

             A18: 1 <= m by A6, A7, XXREAL_0: 2;

            then

             A19: (sc . m) joins (vm,vm1) by A8, A9;

            

             A20: m <= ( len vs) by A8, A11, NAT_1: 12;

            then

             A21: vm = (vs . m) by A18, FINSEQ_4: 15;

            assume

             A22: not thesis;

            per cases by A22, A15, A19;

              suppose

               A23: vn = vm & vn1 = vm1;

              

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

              n = 1 by A6, A7, A10, A20, A17, A21, A23;

              hence contradiction by A10, A12, A16, A13, A23, A24;

            end;

              suppose

               A25: vn = vm1 & vn1 = vm;

              thus contradiction

              proof

                

                 A26: (n + 1) <= m by A7, NAT_1: 13;

                

                 A27: (n + 0 ) < (m + 1) by A7, XREAL_1: 8;

                per cases by A26, XXREAL_0: 1;

                  suppose

                   A28: (n + 1) = m;

                  n = 1 by A6, A10, A12, A17, A13, A25, A27;

                  hence contradiction by A5, A22, A28;

                end;

                  suppose

                   A29: (n + 1) < m;

                  n = 1 by A6, A10, A12, A17, A13, A25, A27;

                  hence contradiction by A10, A20, A16, A21, A25, A29;

                end;

              end;

            end;

          end;

        end;

        hence thesis by GRAPH_1:def 16;

      end;

    end;

    registration

      let G;

      cluster empty -> oriented for Chain of G;

      correctness ;

    end

    definition

      let G;

      let oc be oriented Chain of G;

      assume

       A1: oc <> {} ;

      :: GRAPH_2:def6

      func vertex-seq oc -> FinSequence of the carrier of G means it is_vertex_seq_of oc & (it . 1) = (the Source of G . (oc . 1));

      existence

      proof

        set TG = the Target of G;

        set SG = the Source of G;

        deffunc F( Nat) = (SG . (oc . $1));

        consider z be FinSequence such that

         A2: ( len z) = ( len oc) & for j be Nat st j in ( dom z) holds (z . j) = F(j) from FINSEQ_1:sch 2;

        set vs = (z ^ <*(TG . (oc . ( len oc)))*>);

        

         A3: ( len vs) = (( len oc) + ( len <*(TG . (oc . ( len oc)))*>)) by A2, FINSEQ_1: 22

        .= (( len oc) + 1) by FINSEQ_1: 39;

        

         A4: ( Seg ( len z)) = ( dom z) by FINSEQ_1:def 3;

        

         A5: ( Seg ( len oc)) = ( dom oc) by FINSEQ_1:def 3;

        ( 0 + 1) = 1;

        then

         A6: 1 <= ( len oc) by A1, NAT_1: 13;

        ( rng vs) c= the carrier of G

        proof

          let y be object;

          assume y in ( rng vs);

          then

          consider x be object such that

           A7: x in ( dom vs) and

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

          reconsider x as Element of NAT by A7;

          

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

          

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

          per cases by A3, A10, NAT_1: 8;

            suppose

             A11: x <= ( len oc);

            

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

            

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

            then

             A14: (oc . x) in ( rng oc) by FUNCT_1:def 3;

            then

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

            

             A15: (SG . e) in ( rng the Source of G) by A14, A12, FUNCT_2: 4;

            

             A16: ( rng the Source of G) c= the carrier of G by RELAT_1:def 19;

            (vs . x) = (z . x) by A2, A5, A4, A13, FINSEQ_1:def 7

            .= (SG . e) by A2, A5, A4, A13;

            hence thesis by A8, A15, A16;

          end;

            suppose

             A17: x = (( len oc) + 1);

            ( len oc) in ( dom oc) by A6, FINSEQ_3: 25;

            then

             A18: (oc . ( len oc)) in ( rng oc) by FUNCT_1:def 3;

            

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

            then

            reconsider e = (oc . ( len oc)) as Element of the carrier' of G by A18;

            

             A20: ( rng the Target of G) c= the carrier of G by RELAT_1:def 19;

            (TG . e) in ( rng the Target of G) by A18, A19, FUNCT_2: 4;

            then y is Element of G by A2, A8, A17, A20, FINSEQ_1: 42;

            hence thesis;

          end;

        end;

        then

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

        take vs;

        now

          thus ( len vs) = (( len oc) + 1) by A3;

          let n;

          assume that

           A21: 1 <= n and

           A22: n <= ( len oc);

          

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

          (n + 1) <= ( len vs) by A3, A22, XREAL_1: 7;

          then (n + 1) in ( dom vs) by A23, FINSEQ_3: 25;

          then

          reconsider vsn1 = (vs . (n + 1)) as Element of G by FINSEQ_2: 11;

          

           A24: vsn1 = (vs /. (n + 1)) by A3, A22, A23, FINSEQ_4: 15, XREAL_1: 7;

          

           A25: vsn1 = (TG . (oc . n))

          proof

            per cases by A22, XXREAL_0: 1;

              suppose

               A26: n < ( len oc);

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

              then

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

              

              hence vsn1 = (z . (n + 1)) by A2, A5, A4, FINSEQ_1:def 7

              .= (SG . (oc . (n + 1))) by A2, A5, A4, A27

              .= (TG . (oc . n)) by A21, A26, GRAPH_1:def 15;

            end;

              suppose n = ( len oc);

              hence thesis by A2, FINSEQ_1: 42;

            end;

          end;

          

           A28: n <= ( len vs) by A3, A22, NAT_1: 12;

          then n in ( dom vs) by A21, FINSEQ_3: 25;

          then

          reconsider vsn = (vs . n) as Element of G by FINSEQ_2: 11;

          

           A29: vsn = (vs /. n) by A21, A28, FINSEQ_4: 15;

          

           A30: n in ( dom oc) by A21, A22, FINSEQ_3: 25;

          

          then vsn = (z . n) by A2, A5, A4, FINSEQ_1:def 7

          .= (SG . (oc . n)) by A2, A5, A4, A30;

          hence (oc . n) joins ((vs /. n),(vs /. (n + 1))) by A25, A29, A24;

        end;

        hence vs is_vertex_seq_of oc;

        

         A31: 1 in ( dom z) by A2, A6, FINSEQ_3: 25;

        then (z . 1) = (SG . (oc . 1)) by A2;

        hence thesis by A31, FINSEQ_1:def 7;

      end;

      uniqueness by A1, Th34;

    end