let m, n be Nat; 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; 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; 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; ( 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
; ( 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
; ( 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
; 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; GRAPH_2:def 2 for n being Nat st 1 <= n & n <= len c1 holds
c1 . n joins vs1 /. n,vs1 /. (n + 1)
let k be Nat; ( 1 <= k & k <= len c1 implies c1 . k joins vs1 /. k,vs1 /. (k + 1) )
assume that
A12:
1 <= k
and
A13:
k <= len c1
; 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; verum