let X be non empty set ; :: thesis: for f being FinSequence of X st len f >= 1 holds

ex g being FinSequence of X st g is_Shortcut_of f

let f be FinSequence of X; :: thesis: ( len f >= 1 implies ex g being FinSequence of X st g is_Shortcut_of f )

reconsider f1 = f as FinSequence of the carrier of (PGraph X) ;

assume len f >= 1 ; :: thesis: ex g being FinSequence of X st g is_Shortcut_of f

then consider fc being Subset of (PairF f), fvs being Subset of f1, sc being oriented simple Chain of PGraph X, vs1 being FinSequence of the carrier of (PGraph X) such that

A1: ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & f1 . 1 = vs1 . 1 & f1 . (len f1) = vs1 . (len vs1) ) by Th7, GRAPH_4:21;

reconsider g1 = vs1 as FinSequence of X ;

g1 is_Shortcut_of f by A1;

hence ex g being FinSequence of X st g is_Shortcut_of f ; :: thesis: verum

ex g being FinSequence of X st g is_Shortcut_of f

let f be FinSequence of X; :: thesis: ( len f >= 1 implies ex g being FinSequence of X st g is_Shortcut_of f )

reconsider f1 = f as FinSequence of the carrier of (PGraph X) ;

assume len f >= 1 ; :: thesis: ex g being FinSequence of X st g is_Shortcut_of f

then consider fc being Subset of (PairF f), fvs being Subset of f1, sc being oriented simple Chain of PGraph X, vs1 being FinSequence of the carrier of (PGraph X) such that

A1: ( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & f1 . 1 = vs1 . 1 & f1 . (len f1) = vs1 . (len vs1) ) by Th7, GRAPH_4:21;

reconsider g1 = vs1 as FinSequence of X ;

g1 is_Shortcut_of f by A1;

hence ex g being FinSequence of X st g is_Shortcut_of f ; :: thesis: verum