let G be Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 c is simple Chain of G ; :: thesis: 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) )

then reconsider sc = c as simple Chain of G ;
reconsider fvs = vs as Subset of vs by FINSEQ_6:152;
reconsider fc = c as Subset of c by FINSEQ_6:152;
take fc ; :: thesis: 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) )
take fvs ; :: thesis: 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) )
take sc ; :: thesis: 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) )
take vs ; :: thesis: ( Seq fc = sc & Seq fvs = vs & vs is_vertex_seq_of sc & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) )
thus ( Seq fc = sc & Seq fvs = vs ) by FINSEQ_3:116; :: thesis: ( vs is_vertex_seq_of sc & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) )
thus vs is_vertex_seq_of sc by A1; :: thesis: ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) )
thus ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) ) ; :: thesis: verum

end;

suppose A2: c is not simple Chain of G ; :: thesis: 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 S₁[ 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 );
S₁[ len c]

proof

reconsider fvs = vs as Subset of vs by FINSEQ_6:152;
reconsider fc = c as Subset of c by FINSEQ_6:152;
take fc ; :: thesis: 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 = len c & c1 is not simple Chain of G )
take fvs ; :: thesis: 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 = len c & c1 is not simple Chain of G )
take c ; :: thesis: ex vs1 being FinSequence of the carrier of G st
( Seq fc = c & Seq fvs = vs1 & vs1 is_vertex_seq_of c & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c = len c & c is not simple Chain of G )
take vs ; :: thesis: ( Seq fc = c & Seq fvs = vs & vs is_vertex_seq_of c & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) & len c = len c & c is not simple Chain of G )
thus ( Seq fc = c & Seq fvs = vs ) by FINSEQ_3:116; :: thesis: ( vs is_vertex_seq_of c & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) & len c = len c & c is not simple Chain of G )
thus vs is_vertex_seq_of c by A1; :: thesis: ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) & len c = len c & c is not simple Chain of G )
thus ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) ) ; :: thesis: ( len c = len c & c is not simple Chain of G )
thus ( len c = len c & c is not simple Chain of G ) by A2; :: thesis: verum

end;

then A3: ex k being Nat st S₁[k] ;
consider k being Nat such that
A4: ( S₁[k] & ( for n being Nat st S₁[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; :: thesis: verum

end;

end;