let X be non empty set ; :: thesis: for f, g being FinSequence of X st g is_Shortcut_of f holds
rng () c= rng ()

let f, g be FinSequence of X; :: thesis: ( g is_Shortcut_of f implies rng () c= rng () )
A1: len () = (len g) -' 1 by Def2;
len g < (len g) + 1 by NAT_1:13;
then A2: (len g) - 1 < len g by XREAL_1:19;
assume g is_Shortcut_of f ; :: thesis: rng () c= rng ()
then consider fc being Subset of (), fvs being Subset of f, sc being oriented simple Chain of PGraph X, g1 being FinSequence of the carrier of () such that
A3: Seq fc = sc and
Seq fvs = g and
A4: g1 = g and
A5: g1 is_oriented_vertex_seq_of sc ;
A6: rng (Sgm (dom fc)) = dom fc by FINSEQ_1:50;
fc * (Sgm (dom fc)) = sc by ;
then rng fc = rng sc by ;
then A7: rng sc c= rng () by RELAT_1:11;
len f < (len f) + 1 by NAT_1:13;
then A8: (len f) - 1 < len f by XREAL_1:19;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng () or y in rng () )
assume y in rng () ; :: thesis: y in rng ()
then consider x being object such that
A9: x in dom () and
A10: y = () . x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A9;
A11: x in Seg (len ()) by ;
then A12: 1 <= n by FINSEQ_1:1;
then A13: 1 <= n + 1 by NAT_1:13;
A14: n <= len () by ;
then 1 <= len () by ;
then (len g) -' 1 = (len g) - 1 by ;
then A15: n < len g by ;
then n + 1 <= len g by NAT_1:13;
then n + 1 <= (len sc) + 1 by ;
then A16: n <= len sc by XREAL_1:6;
then A17: sc . n orientedly_joins g1 /. n,g1 /. (n + 1) by ;
n in dom sc by ;
then sc . n in rng sc by FUNCT_1:def 3;
then consider z being object such that
A18: z in dom () and
A19: (PairF f) . z = sc . n by ;
reconsider m = z as Element of NAT by A18;
A20: z in Seg (len ()) by ;
then A21: 1 <= m by FINSEQ_1:1;
m <= len () by ;
then A22: m <= (len f) -' 1 by Def2;
then 1 <= (len f) -' 1 by ;
then (len f) -' 1 = (len f) - 1 by NAT_D:39;
then A23: m < len f by ;
then A24: m + 1 <= len f by NAT_1:13;
A25: 1 <= m by ;
then A26: [(f . m),(f . (m + 1))] = sc . n by ;
1 < m + 1 by ;
then m + 1 in dom f by ;
then A27: f . (m + 1) in rng f by FUNCT_1:def 3;
m in dom f by ;
then A28: f . m in rng f by FUNCT_1:def 3;
then the Source of () . ((f . m),(f . (m + 1))) = f . m by ;
then g1 /. n = f . m by ;
then A29: g . n = f . m by ;
A30: (PairF g) . x = [(g . n),(g . (n + 1))] by ;
the Target of () . ((f . m),(f . (m + 1))) = f . (m + 1) by ;
then A31: g1 /. (n + 1) = f . (m + 1) by ;
n + 1 <= len g1 by ;
then g . (n + 1) = f . (m + 1) by ;
hence y in rng () by ; :: thesis: verum