let q be FinSequence; for m, n being Element of 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 Element of 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 Th10;
A6:
((len q) + m) - m = (n + 1) - m
by A1, A2, A3, A4, GRAPH_2:def 1;
reconsider qq = q as Chain of G by A1, A2, A3, A4, GRAPH_2:44;
for n being Element of 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
Element of
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:11;
then
m - 1
= m -' 1
by XREAL_0:def 2;
then reconsider m1 =
m - 1 as
Element of
NAT ;
reconsider i =
m1 + k as
Element of
NAT ;
set v1 =
vs /. i;
set v2 =
vs /. (i + 1);
0 + 1
<= k
by A7;
then consider j being
Element of
NAT such that
0 <= j
and A9:
j < len q
and A10:
k = j + 1
by A8, GRAPH_2:1;
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, GRAPH_2:def 1;
A13:
c . i = q . k
by A1, A2, A3, A4, A9, A10, A11, GRAPH_2:def 1;
1
- 1
<= m - 1
by A1, XREAL_1:11;
then A14:
0 + 1
<= (m - 1) + k
by A7, XREAL_1:9;
i <= (m - 1) + (n - (m - 1))
by A6, A8, XREAL_1:8;
then
i <= len c
by A3, XXREAL_0:2;
then
c . i orientedly_joins vs /. i,
vs /. (i + 1)
by A5, A14, Def5;
then A15:
the
Target of
G . (c . i) = vs /. (i + 1)
by Def1;
A16:
1
< i + 1
by A14, NAT_1:13;
k + m < n + 1
by A6, A8, XREAL_1:8;
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, Def5;
hence
the
Source of
G . (q . (k + 1)) = the
Target of
G . (q . k)
by A12, A13, A15, Def1;
verum
end;
then
qq is oriented
by GRAPH_1:def 13;
hence
q is oriented Chain of G
; verum