let G be Graph; for vs being FinSequence of the carrier of G
for c being Chain of G st vs is_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex sc being simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
let vs be FinSequence of the carrier of G; for c being Chain of G st vs is_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex sc being simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
let c be Chain of G; ( vs is_vertex_seq_of c implies ex fc being Subset of c ex fvs being Subset of vs ex sc being simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) )
assume A1:
vs is_vertex_seq_of c
; ex fc being Subset of c ex fvs being Subset of vs ex sc being simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
per cases
( c is simple Chain of G or not c is simple Chain of G )
;
suppose A2:
c is not
simple Chain of
G
;
ex fc being Subset of c ex fvs being Subset of vs ex sc being simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )defpred S1[
Nat]
means ex
fc being
Subset of
c ex
fvs being
Subset of
vs ex
c1 being
Chain of
G ex
vs1 being
FinSequence of the
carrier of
G st
(
Seq fc = c1 &
Seq fvs = vs1 &
vs1 is_vertex_seq_of c1 &
vs . 1
= vs1 . 1 &
vs . (len vs) = vs1 . (len vs1) &
len c1 = $1 &
c1 is not
simple Chain of
G );
S1[
len c]
then A3:
ex
k being
Nat st
S1[
k]
;
consider k being
Nat such that A4:
(
S1[
k] & ( for
n being
Nat st
S1[
n] holds
k <= n ) )
from NAT_1:sch 5(A3);
consider fc being
Subset of
c,
fvs being
Subset of
vs,
c1 being
Chain of
G,
vs1 being
FinSequence of the
carrier of
G such that A5:
Seq fc = c1
and A6:
Seq fvs = vs1
and A7:
vs1 is_vertex_seq_of c1
and A8:
vs . 1
= vs1 . 1
and A9:
vs . (len vs) = vs1 . (len vs1)
and A10:
len c1 = k
and A11:
c1 is not
simple Chain of
G
by A4;
consider fc1 being
Subset of
c1,
fvs1 being
Subset of
vs1,
c2 being
Chain of
G,
vs2 being
FinSequence of the
carrier of
G such that A12:
len c2 < len c1
and A13:
vs2 is_vertex_seq_of c2
and
len vs2 < len vs1
and A14:
vs1 . 1
= vs2 . 1
and A15:
vs1 . (len vs1) = vs2 . (len vs2)
and A16:
Seq fc1 = c2
and A17:
Seq fvs1 = vs2
by A7, A11, Th48;
reconsider fc9 =
fc | (rng ((Sgm (dom fc)) | (dom fc1))) as
Subset of
c by FINSEQ_6:153;
reconsider fvs9 =
fvs | (rng ((Sgm (dom fvs)) | (dom fvs1))) as
Subset of
vs by FINSEQ_6:153;
A18:
Seq fvs9 = vs2
by A6, A17, FINSEQ_6:154;
A19:
Seq fc9 = c2
by A5, A16, FINSEQ_6:154;
then
(
c2 is
simple Chain of
G implies ex
fc being
Subset of
c ex
fvs being
Subset of
vs ex
sc being
simple Chain of
G ex
vs1 being
FinSequence of the
carrier of
G st
(
Seq fc = sc &
Seq fvs = vs1 &
vs1 is_vertex_seq_of sc &
vs . 1
= vs1 . 1 &
vs . (len vs) = vs1 . (len vs1) ) )
by A8, A9, A13, A14, A15, A18;
hence
ex
fc being
Subset of
c ex
fvs being
Subset of
vs ex
sc being
simple Chain of
G ex
vs1 being
FinSequence of the
carrier of
G st
(
Seq fc = sc &
Seq fvs = vs1 &
vs1 is_vertex_seq_of sc &
vs . 1
= vs1 . 1 &
vs . (len vs) = vs1 . (len vs1) )
by A4, A8, A9, A10, A12, A13, A14, A15, A19, A18;
verum end; end;