let m, n be Nat; for G being non void Graph
for c being directed Chain of G st 1 <= m & m <= n & n <= len c holds
(m,n) -cut c is directed Chain of G
let G be non void Graph; for c being directed Chain of G st 1 <= m & m <= n & n <= len c holds
(m,n) -cut c is directed Chain of G
let c be directed Chain of G; ( 1 <= m & m <= n & n <= len c implies (m,n) -cut c is directed Chain of G )
assume that
A1:
1 <= m
and
A2:
m <= n
and
A3:
n <= len c
; (m,n) -cut c is directed Chain of G
reconsider mnc = (m,n) -cut c as Chain of G by A1, A2, A3, GRAPH_2:41;
A4:
(len mnc) + m = n + 1
by A1, A2, A3, FINSEQ_6:def 4;
now for k being Nat st 1 <= k & k < len mnc holds
the Source of G . (mnc . (k + 1)) = the Target of G . (mnc . k)A5:
(len mnc) + m <= (len c) + 1
by A3, A4, XREAL_1:6;
let k be
Nat;
( 1 <= k & k < len mnc implies the Source of G . (mnc . (k + 1)) = the Target of G . (mnc . k) )assume that A6:
1
<= k
and A7:
k < len mnc
;
the Source of G . (mnc . (k + 1)) = the Target of G . (mnc . k)
0 + 1
<= k
by A6;
then consider i being
Nat such that
0 <= i
and A8:
i < len mnc
and A9:
k = i + 1
by A7, FINSEQ_6:127;
A10:
1
<= m + i
by A1, NAT_1:12;
m + (i + 1) < (len mnc) + m
by A7, A9, XREAL_1:6;
then
(m + i) + 1
< (len c) + 1
by A5, XXREAL_0:2;
then A11:
m + i < len c
by XREAL_1:6;
A12:
mnc . (k + 1) = c . (m + k)
by A1, A2, A3, A7, FINSEQ_6:def 4;
(
mnc . (i + 1) = c . (m + i) &
m + k = (m + i) + 1 )
by A1, A2, A3, A8, A9, FINSEQ_6:def 4;
hence
the
Source of
G . (mnc . (k + 1)) = the
Target of
G . (mnc . k)
by A12, A10, A11, GRAPH_1:def 15;
verum end;
hence
(m,n) -cut c is directed Chain of G
by GRAPH_1:def 15; verum