let G be Graph; :: thesis: for vs being FinSequence of the carrier of G
for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_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 oriented Chain of G st vs is_oriented_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
let c be oriented Chain of G; :: thesis: ( vs is_oriented_vertex_seq_of c implies ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) )
assume A1: vs is_oriented_vertex_seq_of c ; :: thesis: ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )

per cases ( c is Simple or not c is Simple ) ;

suppose A2: c is Simple ; :: thesis: ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )

reconsider fc = c as Subset of c by GRAPH_2:28;
reconsider fvs = vs as Subset of vs by GRAPH_2:28;
reconsider sc = c as oriented simple Chain of G by A2, Th21;
take fc ; :: thesis: ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
take fvs ; :: thesis: ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_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_oriented_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_oriented_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_oriented_vertex_seq_of sc & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) )
thus vs is_oriented_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: not c is Simple ; :: thesis: ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_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 oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = c1 & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c1 & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c1 = $1 & not c1 is Simple );
S₁[ len c]

proof

reconsider fc = c as Subset of c by GRAPH_2:28;
reconsider fvs = vs as Subset of vs by GRAPH_2:28;
take fc ; :: thesis: ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = c1 & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c1 & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c1 = len c & not c1 is Simple )
take fvs ; :: thesis: ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = c1 & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c1 & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c1 = len c & not c1 is Simple )
take c ; :: thesis: ex vs1 being FinSequence of the carrier of G st
( Seq fc = c & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c = len c & not c is Simple )
take vs ; :: thesis: ( Seq fc = c & Seq fvs = vs & vs is_oriented_vertex_seq_of c & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) & len c = len c & not c is Simple )
thus ( Seq fc = c & Seq fvs = vs ) by FINSEQ_3:125; :: thesis: ( vs is_oriented_vertex_seq_of c & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) & len c = len c & not c is Simple )
thus vs is_oriented_vertex_seq_of c by A1; :: thesis: ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) & len c = len c & not c is Simple )
thus ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) ) ; :: thesis: ( len c = len c & not c is Simple )
thus ( len c = len c & not c is Simple ) 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 oriented Chain of G, vs1 being FinSequence of the carrier of G such that
A6: ( Seq fc = c1 & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c1 & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c1 = k & not c1 is Simple ) by A5;
consider fc1 being Subset of c1, fvs1 being Subset of vs1, c2 being oriented Chain of G, vs2 being FinSequence of the carrier of G such that
A7: ( len c2 < len c1 & vs2 is_oriented_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, Th22;
reconsider fc' = fc | (rng ((Sgm (dom fc)) | (dom fc1))) as Subset of c by GRAPH_2:29;
A8: Seq fc' = c2 by A6, A7, GRAPH_2:30;
reconsider fvs' = fvs | (rng ((Sgm (dom fvs)) | (dom fvs1))) as Subset of vs by GRAPH_2:29;
A9: Seq fvs' = vs2 by A6, A7, GRAPH_2:30;

now

assume c2 is oriented Simple Chain of G ; :: thesis: ex fc' being Subset of c ex sc being oriented simple Chain of G ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
then reconsider sc = c2 as oriented simple Chain of G by Th21;
take fc' = fc'; :: thesis: ex sc being oriented simple Chain of G ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
take sc = sc; :: thesis: ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
Seq fc' = sc by A6, A7, GRAPH_2:30;
hence ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) by A6, A7, A9; :: thesis: verum

end;

hence ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) by A5, A6, A7, A8, A9; :: thesis: verum

end;

end;