let m, n be Nat; :: thesis: for G being Graph

for vs, vs1 being FinSequence of the carrier of G

for c, c1 being Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds

vs1 is_vertex_seq_of c1

let G be Graph; :: thesis: for vs, vs1 being FinSequence of the carrier of G

for c, c1 being Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds

vs1 is_vertex_seq_of c1

let vs, vs1 be FinSequence of the carrier of G; :: thesis: for c, c1 being Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds

vs1 is_vertex_seq_of c1

let c, c1 be Chain of G; :: thesis: ( 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 )

assume that

A1: 1 <= m and

A2: m <= n and

A3: n <= len c ; :: thesis: ( not c1 = (m,n) -cut c or not vs is_vertex_seq_of c or not vs1 = (m,(n + 1)) -cut vs or vs1 is_vertex_seq_of c1 )

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

assume A5: c1 = (m,n) -cut c ; :: thesis: ( not vs is_vertex_seq_of c or not vs1 = (m,(n + 1)) -cut vs or vs1 is_vertex_seq_of c1 )

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 ; :: thesis: vs1 is_vertex_seq_of c1

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; :: according to GRAPH_2:def 2 :: thesis: for n being Nat st 1 <= n & n <= len c1 holds

c1 . n joins vs1 /. n,vs1 /. (n + 1)

let k be Nat; :: thesis: ( 1 <= k & k <= len c1 implies c1 . k joins vs1 /. k,vs1 /. (k + 1) )

assume that

A12: 1 <= k and

A13: k <= len c1 ; :: thesis: c1 . k joins vs1 /. k,vs1 /. (k + 1)

0 + 1 <= k by A12;

then consider j being Nat 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 . (m + j) 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: m + j <= len c by A3, A6, XXREAL_0:2;

then m + j <= len vs by A9, NAT_1:12;

then A18: vs /. (m + j) = vs . (m + j) 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 /. ((m + j) + 1);

set v1 = vs /. (m + j);

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

1 <= m + j by A1, NAT_1:12;

then A24: c . (m + j) joins vs /. (m + j),vs /. ((m + j) + 1) by A7, A17;

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

then A25: vs /. ((m + j) + 1) = vs . ((m + j) + 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 . ((m + j) + 1) by A1, A8, A4, A10, A15, A23, FINSEQ_6:def 4;

hence c1 . k joins vs1 /. k,vs1 /. (k + 1) by A1, A3, A5, A4, A14, A15, A24, A16, A18, A25, A22, A21, Lm2; :: thesis: verum

for vs, vs1 being FinSequence of the carrier of G

for c, c1 being Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds

vs1 is_vertex_seq_of c1

let G be Graph; :: thesis: for vs, vs1 being FinSequence of the carrier of G

for c, c1 being Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds

vs1 is_vertex_seq_of c1

let vs, vs1 be FinSequence of the carrier of G; :: thesis: for c, c1 being Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds

vs1 is_vertex_seq_of c1

let c, c1 be Chain of G; :: thesis: ( 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 )

assume that

A1: 1 <= m and

A2: m <= n and

A3: n <= len c ; :: thesis: ( not c1 = (m,n) -cut c or not vs is_vertex_seq_of c or not vs1 = (m,(n + 1)) -cut vs or vs1 is_vertex_seq_of c1 )

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

assume A5: c1 = (m,n) -cut c ; :: thesis: ( not vs is_vertex_seq_of c or not vs1 = (m,(n + 1)) -cut vs or vs1 is_vertex_seq_of c1 )

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 ; :: thesis: vs1 is_vertex_seq_of c1

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; :: according to GRAPH_2:def 2 :: thesis: for n being Nat st 1 <= n & n <= len c1 holds

c1 . n joins vs1 /. n,vs1 /. (n + 1)

let k be Nat; :: thesis: ( 1 <= k & k <= len c1 implies c1 . k joins vs1 /. k,vs1 /. (k + 1) )

assume that

A12: 1 <= k and

A13: k <= len c1 ; :: thesis: c1 . k joins vs1 /. k,vs1 /. (k + 1)

0 + 1 <= k by A12;

then consider j being Nat 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 . (m + j) 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: m + j <= len c by A3, A6, XXREAL_0:2;

then m + j <= len vs by A9, NAT_1:12;

then A18: vs /. (m + j) = vs . (m + j) 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 /. ((m + j) + 1);

set v1 = vs /. (m + j);

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

1 <= m + j by A1, NAT_1:12;

then A24: c . (m + j) joins vs /. (m + j),vs /. ((m + j) + 1) by A7, A17;

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

then A25: vs /. ((m + j) + 1) = vs . ((m + j) + 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 . ((m + j) + 1) by A1, A8, A4, A10, A15, A23, FINSEQ_6:def 4;

hence c1 . k joins vs1 /. k,vs1 /. (k + 1) by A1, A3, A5, A4, A14, A15, A24, A16, A18, A25, A22, A21, Lm2; :: thesis: verum