let m, n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum