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 ;
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 ;
then (len vs1) + m = (n + 1) + 1 by ;
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 ;
set i = m + j;
j < len vs1 by ;
then A16: vs1 . k = vs . (m + j) by ;
m + k <= (len c1) + m by ;
then ((m + j) + 1) - 1 <= ((len c1) + m) - 1 by ;
then A17: m + j <= len c by ;
then m + j <= len vs by ;
then A18: vs /. (m + j) = vs . (m + j) by ;
A19: k <= len c1 by ;
then A20: k <= len vs1 by ;
1 <= k + 1 by NAT_1:12;
then A21: vs1 /. (k + 1) = vs1 . (k + 1) by ;
0 + 1 = 1 ;
then 1 <= k by ;
then A22: vs1 /. k = vs1 . k by ;
set v2 = vs /. ((m + j) + 1);
set v1 = vs /. (m + j);
A23: (m + j) + 1 = m + (j + 1) ;
1 <= m + j by ;
then A24: c . (m + j) joins vs /. (m + j),vs /. ((m + j) + 1) by ;
1 <= (m + j) + 1 by NAT_1:12;
then A25: vs /. ((m + j) + 1) = vs . ((m + j) + 1) by ;
j + 1 < len vs1 by ;
then vs1 . (k + 1) = vs . ((m + j) + 1) by ;
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