let m, n be Nat; for G being non void Graph
for c, c1 being directed Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c holds
vertex-seq c1 = (m,(n + 1)) -cut (vertex-seq c)
let G be non void Graph; for c, c1 being directed Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c holds
vertex-seq c1 = (m,(n + 1)) -cut (vertex-seq c)
let c, c1 be directed Chain of G; ( 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c implies vertex-seq c1 = (m,(n + 1)) -cut (vertex-seq c) )
assume that
A1:
1 <= m
and
A2:
m <= n
and
A3:
n <= len c
and
A4:
c1 = (m,n) -cut c
; vertex-seq c1 = (m,(n + 1)) -cut (vertex-seq c)
set mn1c = (m,(n + 1)) -cut (vertex-seq c);
A5:
not c is empty
by A1, A2, A3;
then A6:
vertex-seq c is_vertex_seq_of c
by GRAPH_2:def 10;
then A7:
(m,(n + 1)) -cut (vertex-seq c) is_vertex_seq_of c1
by A1, A2, A3, A4, GRAPH_2:42;
set vsc = vertex-seq c;
A8:
m <= n + 1
by A2, NAT_1:12;
A9:
len (vertex-seq c) = (len c) + 1
by A6;
then A10:
n + 1 <= len (vertex-seq c)
by A3, XREAL_1:6;
A11:
not c1 is empty
by A1, A2, A3, A4, A5, Th11;
then
0 < len c1
;
then A12:
c1 . (0 + 1) = c . (m + 0)
by A1, A2, A3, A4, FINSEQ_6:def 4;
A13:
m <= n + 1
by A2, NAT_1:12;
not vertex-seq c is empty
by A9;
then
not (m,(n + 1)) -cut (vertex-seq c) is empty
by A1, A8, A10, Th11;
then
0 < len ((m,(n + 1)) -cut (vertex-seq c))
;
then A14:
(vertex-seq c) . (m + 0) = ((m,(n + 1)) -cut (vertex-seq c)) . (0 + 1)
by A1, A10, A13, FINSEQ_6:def 4;
m <= len c
by A2, A3, XXREAL_0:2;
then
((m,(n + 1)) -cut (vertex-seq c)) . 1 = the Source of G . (c1 . 1)
by A1, A5, A12, A14, Th10;
hence
vertex-seq c1 = (m,(n + 1)) -cut (vertex-seq c)
by A7, A11, GRAPH_2:def 10; verum