let G be Graph; :: thesis: for v being Vertex of G
for c being Element of G -CycleSet st v in G -VSet (rng c) holds
{ c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet )
let v be Vertex of G; :: thesis: for c being Element of G -CycleSet st v in G -VSet (rng c) holds
{ c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet )
let c be Element of G -CycleSet ; :: thesis: ( v in G -VSet (rng c) implies { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet ) )
assume A1:
v in G -VSet (rng c)
; :: thesis: { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet )
then consider vv being Vertex of G such that
A2:
( 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 ) ) )
;
consider e being Element of the carrier' of G such that
A3:
( e in rng c & ( vv = the Source of G . e or vv = the Target of G . e ) )
by A2;
set Cset = { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } ;
reconsider c' = c as cyclic Path of G by Def8;
consider vs being FinSequence of the carrier of G such that
A4:
vs is_vertex_seq_of c'
by GRAPH_2:36;
G -VSet (rng c') = rng vs
by A3, A4, GRAPH_2:34, RELAT_1:60;
then consider n being Nat such that
A5:
( n in dom vs & vs . n = v )
by A1, FINSEQ_2:11;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A6:
len vs = (len c) + 1
by A4, GRAPH_2:def 7;
dom vs = Seg (len vs)
by FINSEQ_1:def 3;
then A7:
( 1 <= n & n <= len vs )
by A5, FINSEQ_1:3;
A8:
now 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 )
;
:: thesis: not { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } is empty then consider m being
Element of
NAT such that A10:
(
n = 1
+ m & 1
<= m )
by FSM_1:1;
A11:
n <= len c
by A6, A9, NAT_1:13;
A12:
m <= m + 1
by NAT_1:11;
then A13:
m <= len c
by A10, A11, XXREAL_0:2;
reconsider c1 = 1,
m -cut c',
c2 =
n,
(len c) -cut c' as
Path of
G by Th8;
set vs1 = 1,
(m + 1) -cut vs;
A14:
( 1
<= (m + 1) + 1 &
m + 1
<= len vs )
by A9, A10, NAT_1:13;
then A15:
(len (1,(m + 1) -cut vs)) + 1
= (m + 1) + 1
by Lm1;
A16:
1,
(m + 1) -cut vs is_vertex_seq_of c1
by A4, A10, A13, GRAPH_2:45;
set vs2 =
n,
(len vs) -cut vs;
A17:
(len (n,(len vs) -cut vs)) + n = (len vs) + 1
by A9, GRAPH_2:def 1;
A18:
n,
(len vs) -cut vs is_vertex_seq_of c2
by A4, A6, A9, A11, GRAPH_2:45;
reconsider vs21 =
(n,(len vs) -cut vs) ^' (1,(m + 1) -cut vs) as
FinSequence of the
carrier of
G ;
then A19:
0 < len (n,(len vs) -cut vs)
;
then A20:
1
+ 0 <= len (n,(len vs) -cut vs)
by NAT_1:13;
then A21:
vs21 . 1 =
(n,(len vs) -cut vs) . (0 + 1)
by GRAPH_2:14
.=
vs . (n + 0 )
by A9, A19, GRAPH_2:def 1
;
consider lv2 being
Element of
NAT such that A22:
(
0 <= lv2 &
lv2 < len (n,(len vs) -cut vs) &
len (n,(len vs) -cut vs) = lv2 + 1 )
by A20, GRAPH_2:1;
A23:
(1,(m + 1) -cut vs) . 1
= vs . (1 + 0 )
by A14, A15, Lm1;
A24:
(n,(len vs) -cut vs) . (len (n,(len vs) -cut vs)) =
vs . (n + lv2)
by A9, A22, GRAPH_2:def 1
.=
(1,(m + 1) -cut vs) . 1
by A4, A17, A22, A23, MSSCYC_1:6
;
now given y being
set such that A25:
(
y in rng c1 &
y in rng c2 )
;
:: thesis: contradictionconsider a being
Nat such that A26:
(
a in dom c1 &
c1 . a = y )
by A25, FINSEQ_2:11;
consider b being
Nat such that A27:
(
b in dom c2 &
c2 . b = y )
by A25, FINSEQ_2:11;
consider k being
Element of
NAT such that A28:
(
k in dom c' &
c . k = c1 . a &
k + 1
= 1
+ a & 1
<= k &
k <= m )
by A26, Th2;
consider l being
Element of
NAT such that A29:
(
l in dom c' &
c . l = c2 . b &
l + 1
= n + b &
n <= l &
l <= len c )
by A27, Th2;
k < n
by A10, A28, NAT_1:13;
hence
contradiction
by A26, A27, A28, A29, FUNCT_1:def 8;
:: thesis: verum end; then
rng c1 misses rng c2
by XBOOLE_0:3;
then reconsider c21' =
c2 ^ c1 as
Path of
G by A16, A18, A24, Th9;
A30:
vs21 is_vertex_seq_of c21'
by A16, A18, A24, GRAPH_2:47;
1
< len (1,(m + 1) -cut vs)
by A10, A15, NAT_1:13;
then vs21 . (len vs21) =
(1,(m + 1) -cut vs) . (len (1,(m + 1) -cut vs))
by GRAPH_2:16
.=
vs . n
by A9, A10, GRAPH_2:12
;
then reconsider c21' =
c21' as
cyclic Path of
G by A21, A30, MSSCYC_1:def 2;
reconsider c21 =
c21' as
Element of
G -CycleSet by Def8;
A31:
c = c1 ^ c2
by A10, A11, A12, GRAPH_2:9, XXREAL_0:2;
rng c21 =
(rng c2) \/ (rng c1)
by FINSEQ_1:44
.=
rng c
by A31, FINSEQ_1:44
;
then
c21 in { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) }
by A5, A21, A30;
hence
not
{ c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } is
empty
;
:: thesis: verum end;
{ c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } c= G -CycleSet
hence
{ c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet )
by A8; :: thesis: verum