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 , fvs being Subset of , 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 Th11, GRAPH_4:23;
reconsider g1 = vs1 as FinSequence of X ;
g1 is_Shortcut_of f by A1, Def3;
hence ex g being FinSequence of X st g is_Shortcut_of f ; :: thesis: verum