let m, n be Nat; for G being Graph
for vs, vs1 being FinSequence of the carrier of G
for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds
vs1 is_oriented_vertex_seq_of c1
let G be Graph; for vs, vs1 being FinSequence of the carrier of G
for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds
vs1 is_oriented_vertex_seq_of c1
let vs, vs1 be FinSequence of the carrier of G; for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds
vs1 is_oriented_vertex_seq_of c1
let c, c1 be oriented Chain of G; ( 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs implies vs1 is_oriented_vertex_seq_of c1 )
assume that
A1:
1 <= m
and
A2:
m <= n
and
A3:
n <= len c
; ( not c1 = (m,n) -cut c or not vs is_oriented_vertex_seq_of c or not vs1 = (m,(n + 1)) -cut vs or vs1 is_oriented_vertex_seq_of c1 )
assume A4:
c1 = (m,n) -cut c
; ( not vs is_oriented_vertex_seq_of c or not vs1 = (m,(n + 1)) -cut vs or vs1 is_oriented_vertex_seq_of c1 )
assume that
A5:
vs is_oriented_vertex_seq_of c
and
A6:
vs1 = (m,(n + 1)) -cut vs
; vs1 is_oriented_vertex_seq_of c1
A7:
len vs = (len c) + 1
by A5;
A8:
m <= n + 1
by A2, NAT_1:12;
A9:
n + 1 <= len vs
by A3, A7, XREAL_1:6;
A10:
(len c1) + m = n + 1
by A1, A2, A3, A4, FINSEQ_6:def 4;
(len vs1) + m = (n + 1) + 1
by A1, A6, A8, A9, FINSEQ_6:def 4;
hence A11:
len vs1 = (len c1) + 1
by A10; GRAPH_4:def 5 for n being Nat st 1 <= n & n <= len c1 holds
c1 . n orientedly_joins vs1 /. n,vs1 /. (n + 1)
let k be Nat; ( 1 <= k & k <= len c1 implies c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) )
assume that
A12:
1 <= k
and
A13:
k <= len c1
; c1 . k orientedly_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;
set v1 = vs /. (m + j);
set v2 = vs /. ((m + j) + 1);
m + k <= (len c1) + m
by A13, XREAL_1:7;
then A16:
((m + j) + 1) - 1 <= ((len c1) + m) - 1
by A15, XREAL_1:9;
A17:
1 <= m + j
by A1, NAT_1:12;
A18:
m + j <= len c
by A3, A10, A16, XXREAL_0:2;
then A19:
c . (m + j) orientedly_joins vs /. (m + j),vs /. ((m + j) + 1)
by A5, A17;
j < len vs1
by A11, A14, NAT_1:13;
then A20:
vs1 . k = vs . (m + j)
by A1, A6, A8, A9, A15, FINSEQ_6:def 4;
A21:
j + 1 < len vs1
by A11, A14, XREAL_1:6;
(m + j) + 1 = m + (j + 1)
;
then A22:
vs1 . (k + 1) = vs . ((m + j) + 1)
by A1, A6, A8, A9, A15, A21, FINSEQ_6:def 4;
A23:
m + j <= len vs
by A7, A18, NAT_1:12;
A24:
1 <= (m + j) + 1
by NAT_1:12;
A25:
vs /. (m + j) = vs . (m + j)
by A1, A23, FINSEQ_4:15, NAT_1:12;
A26:
vs /. ((m + j) + 1) = vs . ((m + j) + 1)
by A7, A18, A24, FINSEQ_4:15, XREAL_1:7;
0 + 1 = 1
;
then A27:
1 <= k
by A15, NAT_1:13;
A28:
k <= len c1
by A14, A15, NAT_1:13;
then A29:
k <= len vs1
by A11, NAT_1:12;
A30:
1 <= k + 1
by NAT_1:12;
A31:
vs1 /. k = vs1 . k
by A27, A29, FINSEQ_4:15;
vs1 /. (k + 1) = vs1 . (k + 1)
by A11, A28, A30, FINSEQ_4:15, XREAL_1:7;
hence
c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1)
by A1, A2, A3, A4, A14, A15, A19, A20, A22, A25, A26, A31, FINSEQ_6:def 4; verum