let G be non void Graph; for c being non empty directed Chain of G st c is cyclic holds
for n being Nat ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
let c be non empty directed Chain of G; ( c is cyclic implies for n being Nat ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G ) )
defpred S1[ Nat] means ex ch being directed Chain of G st
( rng ch c= rng c & len ch = $1 & ch ^ c is non empty directed Chain of G );
c is FinSequence of the carrier' of G
by Def1;
then A1:
rng c c= the carrier' of G
by FINSEQ_1:def 4;
assume A2:
c is cyclic
; for n being Nat ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
A3:
for i being Nat st S1[i] holds
S1[i + 1]
proof
len c in dom c
by FINSEQ_5:6;
then A4:
c . (len c) in rng c
by FUNCT_1:def 3;
then reconsider clc =
c . (len c) as
Element of the
carrier' of
G by A1;
reconsider ch9 =
<*clc*> as
directed Chain of
G by Th4;
A5:
rng ch9 = {(c . (len c))}
by FINSEQ_1:38;
then A6:
rng ch9 c= rng c
by A4, ZFMISC_1:31;
A7:
len ch9 = 1
by FINSEQ_1:39;
let n be
Nat;
( S1[n] implies S1[n + 1] )
given ch being
directed Chain of
G such that A8:
rng ch c= rng c
and A9:
len ch = n
and A10:
ch ^ c is non
empty directed Chain of
G
;
S1[n + 1]
per cases
( n = 0 or n <> 0 )
;
suppose
n <> 0
;
S1[n + 1]then A12:
not
ch is
empty
by A9;
then
1
in dom ch
by FINSEQ_5:6;
then
ch . 1
in rng ch
by FUNCT_1:def 3;
then consider i being
Nat such that A13:
i in dom c
and A14:
c . i = ch . 1
by A8, FINSEQ_2:10;
A15:
i <= len c
by A13, FINSEQ_3:25;
A16:
1
<= i
by A13, FINSEQ_3:25;
now ex ch1 being directed Chain of G st
( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )per cases
( i = 1 or i <> 1 )
;
suppose A17:
i = 1
;
ex ch1 being directed Chain of G st
( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )set vsch9 =
vertex-seq ch9;
vertex-seq ch9 = <*( the Source of G . clc),( the Target of G . clc)*>
by Th6;
then (vertex-seq ch9) . ((len ch9) + 1) =
the
Target of
G . clc
by A7
.=
(vertex-seq c) . ((len c) + 1)
by Th13
.=
(vertex-seq c) . 1
by A2, Th16
.=
the
Source of
G . (ch . 1)
by A14, A17, GRAPH_2:def 10
.=
(vertex-seq ch) . 1
by A12, GRAPH_2:def 10
;
then reconsider ch1 =
ch9 ^ ch as
directed Chain of
G by A12, Th14;
take ch1 =
ch1;
( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )
rng ch1 = (rng ch9) \/ (rng ch)
by FINSEQ_1:31;
hence
rng ch1 c= rng c
by A8, A6, XBOOLE_1:8;
( len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )thus
len ch1 = n + 1
by A9, A7, FINSEQ_1:22;
ch1 ^ c is non empty directed Chain of G(vertex-seq ch1) . ((len ch1) + 1) =
(vertex-seq ch) . ((len ch) + 1)
by A12, Th15
.=
(vertex-seq c) . 1
by A10, A12, Th14
;
hence
ch1 ^ c is non
empty directed Chain of
G
by Th14;
verum end; suppose
i <> 1
;
ex ch1 being directed Chain of G st
( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )then
1
< i
by A16, XXREAL_0:1;
then
1
+ 1
<= i
by NAT_1:13;
then consider k being
Nat such that A18:
( 1
<= k &
k < len c )
and A19:
i = k + 1
by A15, FINSEQ_6:127;
k in dom c
by A18, FINSEQ_3:25;
then A20:
c . k in rng c
by FUNCT_1:def 3;
then reconsider ck =
c . k as
Element of the
carrier' of
G by A1;
reconsider ch9 =
<*ck*> as
directed Chain of
G by Th4;
set vsch9 =
vertex-seq ch9;
A21:
len ch9 = 1
by FINSEQ_1:39;
vertex-seq ch9 = <*( the Source of G . ck),( the Target of G . ck)*>
by Th6;
then (vertex-seq ch9) . ((len ch9) + 1) =
the
Target of
G . ck
by A21
.=
the
Source of
G . (ch . 1)
by A14, A18, A19, GRAPH_1:def 15
.=
(vertex-seq ch) . 1
by A12, GRAPH_2:def 10
;
then reconsider ch1 =
ch9 ^ ch as
directed Chain of
G by A12, Th14;
take ch1 =
ch1;
( rng ch1 c= rng c & len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )
rng ch9 = {(c . k)}
by FINSEQ_1:38;
then A22:
rng ch9 c= rng c
by A20, ZFMISC_1:31;
rng ch1 = (rng ch9) \/ (rng ch)
by FINSEQ_1:31;
hence
rng ch1 c= rng c
by A8, A22, XBOOLE_1:8;
( len ch1 = n + 1 & ch1 ^ c is non empty directed Chain of G )thus
len ch1 = n + 1
by A9, A21, FINSEQ_1:22;
ch1 ^ c is non empty directed Chain of G(vertex-seq ch1) . ((len ch1) + 1) =
(vertex-seq ch) . ((len ch) + 1)
by A12, Th15
.=
(vertex-seq c) . 1
by A10, A12, Th14
;
hence
ch1 ^ c is non
empty directed Chain of
G
by Th14;
verum end; hence
S1[
n + 1]
;
verum end;
end;
let n be Nat; ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
A23:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A23, A3);
then
ex ch being directed Chain of G st
( rng ch c= rng c & len ch = n & ch ^ c is non empty directed Chain of G )
;
hence
ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
; verum