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:78 ;
assume g is_Shortcut_of f ; :: thesis: ( 1 <= len g & len g <= len f )
then consider fc being Subset of , fvs being Subset of , 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 by Def3;
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:71;
A7: dom fvs c= dom f by RELAT_1:25;
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:46;
then len g = len (Sgm (dom fvs)) by FINSEQ_3:31
.= card dfvs by A8, FINSEQ_3:44 ;
hence ( 1 <= len g & len g <= len f ) by A3, A5, A7, A1, NAT_1:12, NAT_1:44; :: thesis: verum