let X be non empty set ; :: thesis: for f, g being FinSequence of X st g is_Shortcut_of f holds
( 1 <= len g & len g <= len f )
let f, g be FinSequence of X; :: thesis: ( g is_Shortcut_of f implies ( 1 <= len g & len g <= len f ) )
reconsider df = dom f as finite set ;
A1: card df = card (Seg (len f)) by FINSEQ_1:def 3
.= len f by FINSEQ_1:57 ;
assume g is_Shortcut_of f ; :: thesis: ( 1 <= len g & len g <= len f )
then consider fc being Subset of (PairF f), fvs being Subset of f, sc being oriented simple Chain of PGraph X, g1 being FinSequence of the carrier of (PGraph X) such that
Seq fc = sc and
A2: Seq fvs = g and
A3: g1 = g and
A4: g1 is_oriented_vertex_seq_of sc ;
A5: len g1 = (len sc) + 1 by A4, GRAPH_4:def 5;
reconsider dfvs = dom fvs as finite set ;
A6: rng (Sgm (dom fvs)) c= dom fvs by FINSEQ_1:50;
A7: dom fvs c= dom f by RELAT_1:11;
then A8: dom fvs c= Seg (len f) by FINSEQ_1:def 3;
g = fvs * (Sgm (dom fvs)) by A2, FINSEQ_1:def 14;
then dom g = dom (Sgm (dom fvs)) by A6, RELAT_1:27;
then len g = len (Sgm (dom fvs)) by FINSEQ_3:29
.= card dfvs by A8, FINSEQ_3:39 ;
hence ( 1 <= len g & len g <= len f ) by A3, A5, A7, A1, NAT_1:12, NAT_1:43; :: thesis: verum