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 A2: 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) )

reconsider fc = c as Subset of c by Th28;
reconsider fvs = vs as Subset of vs by Th28;
reconsider sc = c as simple Chain of G by A2;
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:125; :: 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 A3: 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 fc = c as Subset of c by Th28;
reconsider fvs = vs as Subset of vs by Th28;
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:125; :: 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 A3; :: thesis: verum

end;

then A4: ex k being Nat st S₁[k] ;
consider k being Nat such that
A5: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A4);
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
A6: ( Seq fc = c1 & Seq fvs = vs1 & vs1 is_vertex_seq_of c1 & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c1 = k & c1 is not simple Chain of G ) by A5;
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
A7: ( len c2 < len c1 & vs2 is_vertex_seq_of c2 & len vs2 < len vs1 & vs1 . 1 = vs2 . 1 & vs1 . (len vs1) = vs2 . (len vs2) & Seq fc1 = c2 & Seq fvs1 = vs2 ) by A6, Th52;
reconsider fc' = fc | (rng ((Sgm (dom fc)) | (dom fc1))) as Subset of c by Th29;
A8: Seq fc' = c2 by A6, A7, Th30;
reconsider fvs' = fvs | (rng ((Sgm (dom fvs)) | (dom fvs1))) as Subset of vs by Th29;
A9: Seq fvs' = vs2 by A6, A7, Th30;
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 A6, A7, A8;
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 A5, A6, A7, A8, A9; :: thesis: verum

end;

end;