let q be FinSequence; for m, n being Nat
for G being Graph
for c being Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is Chain of G
let m, n be Nat; for G being Graph
for c being Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is Chain of G
let G be Graph; for c being Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is Chain of G
let c be Chain of G; ( 1 <= m & m <= n & n <= len c & q = (m,n) -cut c implies q is Chain of G )
assume that
A1:
1 <= m
and
A2:
m <= n
and
A3:
n <= len c
; ( not q = (m,n) -cut c or q is Chain of G )
A4:
m <= n + 1
by A2, NAT_1:12;
consider vs being FinSequence of the carrier of G such that
A5:
vs is_vertex_seq_of c
by Th33;
set p9 = (m,(n + 1)) -cut vs;
A6:
now for k being Nat st 1 <= k & k <= len ((m,(n + 1)) -cut vs) holds
((m,(n + 1)) -cut vs) . k in the carrier of Glet k be
Nat;
( 1 <= k & k <= len ((m,(n + 1)) -cut vs) implies ((m,(n + 1)) -cut vs) . k in the carrier of G )assume that A7:
1
<= k
and A8:
k <= len ((m,(n + 1)) -cut vs)
;
((m,(n + 1)) -cut vs) . k in the carrier of G
k in dom ((m,(n + 1)) -cut vs)
by A7, A8, FINSEQ_3:25;
then A9:
((m,(n + 1)) -cut vs) . k in rng ((m,(n + 1)) -cut vs)
by FUNCT_1:def 3;
A10:
rng vs c= the
carrier of
G
by FINSEQ_1:def 4;
rng ((m,(n + 1)) -cut vs) c= rng vs
by FINSEQ_6:137;
hence
((m,(n + 1)) -cut vs) . k in the
carrier of
G
by A10, A9;
verum end;
assume A11:
q = (m,n) -cut c
; q is Chain of G
then A12:
((len q) + m) - m = (n + 1) - m
by A1, A3, A4, Lm2;
A13:
len vs = (len c) + 1
by A5;
then A14:
n + 1 <= len vs
by A3, XREAL_1:6;
then A15:
((len ((m,(n + 1)) -cut vs)) + m) - m = ((n + 1) + 1) - m
by A1, A4, FINSEQ_6:def 4;
then A16:
len ((m,(n + 1)) -cut vs) = ((n - m) + 1) + 1
;
A17:
now for k being Nat st 1 <= k & k <= len q holds
ex v1, v2 being Element of the carrier of G st
( v1 = ((m,(n + 1)) -cut vs) . k & v2 = ((m,(n + 1)) -cut vs) . (k + 1) & q . k joins v1,v2 )
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 ;
let k be
Nat;
( 1 <= k & k <= len q implies ex v1, v2 being Element of the carrier of G st
( v1 = ((m,(n + 1)) -cut vs) . k & v2 = ((m,(n + 1)) -cut vs) . (k + 1) & q . k joins v1,v2 ) )reconsider i =
m1 + k as
Nat ;
assume that A18:
1
<= k
and A19:
k <= len q
;
ex v1, v2 being Element of the carrier of G st
( v1 = ((m,(n + 1)) -cut vs) . k & v2 = ((m,(n + 1)) -cut vs) . (k + 1) & q . k joins v1,v2 )
0 + 1
<= k
by A18;
then consider j being
Nat such that
0 <= j
and A20:
j < len q
and A21:
k = j + 1
by A19, FINSEQ_6:127;
A22:
j + 1
< len ((m,(n + 1)) -cut vs)
by A12, A16, A20, XREAL_1:6;
i + 1
= m + (j + 1)
by A21;
then A23:
((m,(n + 1)) -cut vs) . (k + 1) = vs . (i + 1)
by A1, A4, A14, A22, FINSEQ_6:def 4;
set v2 =
vs /. (i + 1);
set v1 =
vs /. i;
A24:
1
<= i + 1
by NAT_1:12;
A25:
i = m + j
by A21;
j < len ((m,(n + 1)) -cut vs)
by A12, A16, A20, NAT_1:13;
then A26:
((m,(n + 1)) -cut vs) . k = vs . i
by A1, A4, A14, A25, A22, FINSEQ_6:def 4;
i <= (m - 1) + (n - (m - 1))
by A12, A19, XREAL_1:6;
then A27:
i <= len c
by A3, XXREAL_0:2;
then A28:
i <= len vs
by A13, NAT_1:12;
take v1 =
vs /. i;
ex v2 being Element of the carrier of G st
( v1 = ((m,(n + 1)) -cut vs) . k & v2 = ((m,(n + 1)) -cut vs) . (k + 1) & q . k joins v1,v2 )take v2 =
vs /. (i + 1);
( v1 = ((m,(n + 1)) -cut vs) . k & v2 = ((m,(n + 1)) -cut vs) . (k + 1) & q . k joins v1,v2 )A29:
i + 1
<= len vs
by A13, A27, XREAL_1:7;
1
- 1
<= m - 1
by A1, XREAL_1:9;
then A30:
0 + 1
<= (m - 1) + k
by A18, XREAL_1:7;
then
c . i joins v1,
v2
by A5, A27;
hence
(
v1 = ((m,(n + 1)) -cut vs) . k &
v2 = ((m,(n + 1)) -cut vs) . (k + 1) &
q . k joins v1,
v2 )
by A1, A3, A11, A4, A20, A21, A25, A30, A28, A24, A29, A26, A23, Lm2, FINSEQ_4:15;
verum
thus
q is Chain of G
verumproof
take
(
m,
(n + 1))
-cut vs
;
( len ((m,(n + 1)) -cut vs) = (len q) + 1 & ( for b1 being set holds
( not 1 <= b1 or not b1 <= len ((m,(n + 1)) -cut vs) or ((m,(n + 1)) -cut vs) . b1 in the carrier of G ) ) & ( for b1 being set holds
( not 1 <= b1 or not b1 <= len q or ex b2, b3 being Element of the carrier of G st
( b2 = ((m,(n + 1)) -cut vs) . b1 & b3 = ((m,(n + 1)) -cut vs) . (b1 + 1) & q . b1 joins b2,b3 ) ) ) )
thus
len ((m,(n + 1)) -cut vs) = (len q) + 1
by A12, A15;
( ( for b1 being set holds
( not 1 <= b1 or not b1 <= len ((m,(n + 1)) -cut vs) or ((m,(n + 1)) -cut vs) . b1 in the carrier of G ) ) & ( for b1 being set holds
( not 1 <= b1 or not b1 <= len q or ex b2, b3 being Element of the carrier of G st
( b2 = ((m,(n + 1)) -cut vs) . b1 & b3 = ((m,(n + 1)) -cut vs) . (b1 + 1) & q . b1 joins b2,b3 ) ) ) )
thus
for
n being
Nat st 1
<= n &
n <= len ((m,(n + 1)) -cut vs) holds
((m,(n + 1)) -cut vs) . n in the
carrier of
G
by A6;
for b1 being set holds
( not 1 <= b1 or not b1 <= len q or ex b2, b3 being Element of the carrier of G st
( b2 = ((m,(n + 1)) -cut vs) . b1 & b3 = ((m,(n + 1)) -cut vs) . (b1 + 1) & q . b1 joins b2,b3 ) )
thus
for
b1 being
set holds
( not 1
<= b1 or not
b1 <= len q or ex
b2,
b3 being
Element of the
carrier of
G st
(
b2 = ((m,(n + 1)) -cut vs) . b1 &
b3 = ((m,(n + 1)) -cut vs) . (b1 + 1) &
q . b1 joins b2,
b3 ) )
by A17;
verum
end;