let G be Graph; for v being Vertex of G
for c being Element of G -CycleSet st v in G -VSet (rng c) holds
{ c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet)
let v be Vertex of G; for c being Element of G -CycleSet st v in G -VSet (rng c) holds
{ c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet)
let c be Element of G -CycleSet ; ( v in G -VSet (rng c) implies { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet) )
set Cset = { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } ;
reconsider c9 = c as cyclic Path of G by Def8;
consider vs being FinSequence of the carrier of G such that
A1:
vs is_vertex_seq_of c9
by GRAPH_2:33;
A2:
len vs = (len c) + 1
by A1;
assume A3:
v in G -VSet (rng c)
; { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet)
then A4:
ex vv being Vertex of G st
( vv = v & ex e being Element of the carrier' of G st
( e in rng c & ( vv = the Source of G . e or vv = the Target of G . e ) ) )
;
then
G -VSet (rng c9) = rng vs
by A1, GRAPH_2:31, RELAT_1:38;
then consider n being Nat such that
A5:
n in dom vs
and
A6:
vs . n = v
by A3, FINSEQ_2:10;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
dom vs = Seg (len vs)
by FINSEQ_1:def 3;
then A7:
( 1 <= n & n <= len vs )
by A5, FINSEQ_1:1;
A8:
now not { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } is empty per cases
( ( 1 = n & n = len vs ) or 1 = n or n = len vs or ( 1 < n & n < len vs ) )
by A7, XXREAL_0:1;
suppose A9:
( 1
< n &
n < len vs )
;
not { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } is empty set vs2 = (
n,
(len vs))
-cut vs;
consider m being
Element of
NAT such that A10:
n = 1
+ m
and A11:
1
<= m
by A9, FINSEQ_4:84;
set vs1 = (1,
(m + 1))
-cut vs;
A12:
1
<= (m + 1) + 1
by A9, A10, NAT_1:13;
then A13:
(len ((1,(m + 1)) -cut vs)) + 1
= (m + 1) + 1
by A9, A10, Lm1;
then A14:
((1,(m + 1)) -cut vs) . 1
= vs . (1 + 0)
by A9, A10, A12, Lm1;
reconsider c1 = (1,
m)
-cut c9,
c2 = (
n,
(len c))
-cut c9 as
Path of
G by Th5;
A15:
n <= len c
by A2, A9, NAT_1:13;
then A16:
(
n,
(len vs))
-cut vs is_vertex_seq_of c2
by A1, A9, GRAPH_2:42;
A17:
(len ((n,(len vs)) -cut vs)) + n = (len vs) + 1
by A9, FINSEQ_6:def 4;
then A19:
1
+ 0 <= len ((n,(len vs)) -cut vs)
by NAT_1:13;
then consider lv2 being
Nat such that
0 <= lv2
and A20:
lv2 < len ((n,(len vs)) -cut vs)
and A21:
len ((n,(len vs)) -cut vs) = lv2 + 1
by FINSEQ_6:127;
reconsider vs21 =
((n,(len vs)) -cut vs) ^' ((1,(m + 1)) -cut vs) as
FinSequence of the
carrier of
G ;
A22:
vs21 . 1 =
((n,(len vs)) -cut vs) . (0 + 1)
by A19, FINSEQ_6:140
.=
vs . (n + 0)
by A9, A18, FINSEQ_6:def 4
;
A23:
m <= m + 1
by NAT_1:11;
then
m <= len c
by A10, A15, XXREAL_0:2;
then A24:
(1,
(m + 1))
-cut vs is_vertex_seq_of c1
by A1, A11, GRAPH_2:42;
A25:
((n,(len vs)) -cut vs) . (len ((n,(len vs)) -cut vs)) =
vs . (n + lv2)
by A9, A20, A21, FINSEQ_6:def 4
.=
((1,(m + 1)) -cut vs) . 1
by A1, A17, A21, A14, MSSCYC_1:6
;
now for y being object holds
( not y in rng c1 or not y in rng c2 )given y being
object such that A26:
y in rng c1
and A27:
y in rng c2
;
contradictionconsider b being
Nat such that A28:
b in dom c2
and A29:
c2 . b = y
by A27, FINSEQ_2:10;
A30:
ex
l being
Nat st
(
l in dom c9 &
c . l = c2 . b &
l + 1
= n + b &
n <= l &
l <= len c )
by A28, Th2;
consider a being
Nat such that A31:
a in dom c1
and A32:
c1 . a = y
by A26, FINSEQ_2:10;
consider k being
Nat such that A33:
(
k in dom c9 &
c . k = c1 . a )
and
k + 1
= 1
+ a
and
1
<= k
and A34:
k <= m
by A31, Th2;
k < n
by A10, A34, NAT_1:13;
hence
contradiction
by A32, A29, A33, A30, FUNCT_1:def 4;
verum end; then
rng c1 misses rng c2
by XBOOLE_0:3;
then reconsider c219 =
c2 ^ c1 as
Path of
G by A24, A16, A25, Th6;
A35:
vs21 is_vertex_seq_of c219
by A24, A16, A25, GRAPH_2:44;
A36:
c = c1 ^ c2
by A10, A15, A23, FINSEQ_6:135, XXREAL_0:2;
1
< len ((1,(m + 1)) -cut vs)
by A11, A13, NAT_1:13;
then vs21 . (len vs21) =
((1,(m + 1)) -cut vs) . (len ((1,(m + 1)) -cut vs))
by FINSEQ_6:142
.=
vs . n
by A9, A10, FINSEQ_6:138
;
then reconsider c219 =
c219 as
cyclic Path of
G by A22, A35, MSSCYC_1:def 2;
reconsider c21 =
c219 as
Element of
G -CycleSet by Def8;
rng c21 =
(rng c2) \/ (rng c1)
by FINSEQ_1:31
.=
rng c
by A36, FINSEQ_1:31
;
then
c21 in { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) }
by A6, A22, A35;
hence
not
{ c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } is
empty
;
verum end;
{ c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } c= G -CycleSet
hence
{ c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet)
by A8; verum