let q be FinSequence; for m, n being Nat
for G being Graph
for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is oriented Chain of G
let m, n be Nat; for G being Graph
for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is oriented Chain of G
let G be Graph; for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is oriented Chain of G
let c be oriented Chain of G; ( 1 <= m & m <= n & n <= len c & q = (m,n) -cut c implies q is oriented Chain of G )
assume that
A1:
1 <= m
and
A2:
m <= n
and
A3:
n <= len c
and
A4:
q = (m,n) -cut c
; q is oriented Chain of G
consider vs being FinSequence of the carrier of G such that
A5:
vs is_oriented_vertex_seq_of c
by Th9;
A6:
((len q) + m) - m = (n + 1) - m
by A1, A2, A3, A4, FINSEQ_6:def 4;
reconsider qq = q as Chain of G by A1, A2, A3, A4, GRAPH_2:41;
for n being Nat st 1 <= n & n < len q holds
the Source of G . (q . (n + 1)) = the Target of G . (q . n)
proof
let k be
Nat;
( 1 <= k & k < len q implies the Source of G . (q . (k + 1)) = the Target of G . (q . k) )
assume that A7:
1
<= k
and A8:
k < len q
;
the Source of G . (q . (k + 1)) = the Target of G . (q . k)
1
- 1
<= m - 1
by A1, XREAL_1:9;
then
m - 1
= m -' 1
by XREAL_0:def 2;
then reconsider m1 =
m - 1 as
Element of
NAT ;
reconsider i =
m1 + k as
Nat ;
set v1 =
vs /. i;
set v2 =
vs /. (i + 1);
0 + 1
<= k
by A7;
then consider j being
Nat such that
0 <= j
and A9:
j < len q
and A10:
k = j + 1
by A8, FINSEQ_6:127;
A11:
i = m + j
by A10;
i + 1
= m + (j + 1)
by A10;
then A12:
c . (i + 1) = q . (k + 1)
by A1, A2, A3, A4, A8, FINSEQ_6:def 4;
A13:
c . i = q . k
by A1, A2, A3, A4, A9, A10, A11, FINSEQ_6:def 4;
1
- 1
<= m - 1
by A1, XREAL_1:9;
then A14:
0 + 1
<= (m - 1) + k
by A7, XREAL_1:7;
i <= (m - 1) + (n - (m - 1))
by A6, A8, XREAL_1:6;
then
i <= len c
by A3, XXREAL_0:2;
then
c . i orientedly_joins vs /. i,
vs /. (i + 1)
by A5, A14;
then A15:
the
Target of
G . (c . i) = vs /. (i + 1)
;
A16:
1
< i + 1
by A14, NAT_1:13;
k + m < n + 1
by A6, A8, XREAL_1:6;
then
k + m <= n
by NAT_1:13;
then
m + k <= len c
by A3, XXREAL_0:2;
then
c . (i + 1) orientedly_joins vs /. (i + 1),
vs /. ((i + 1) + 1)
by A5, A16;
hence
the
Source of
G . (q . (k + 1)) = the
Target of
G . (q . k)
by A12, A13, A15;
verum
end;
then
qq is oriented
by GRAPH_1:def 15;
hence
q is oriented Chain of G
; verum