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

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 )
;

end;

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

( 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;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

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

( Seq fc = sc & Seq fvs = vs1 & vs1 is_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )

defpred S_{1}[ 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_{1}[ len c]
_{1}[k]
;

consider k being Nat such that

A4: ( S_{1}[k] & ( for n being Nat st S_{1}[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;( 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

proof

then A3:
ex k being Nat st S
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;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

consider k being Nat such that

A4: ( S

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