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