let X be non empty set ; :: thesis: for f, g being FinSequence of X st g is_Shortcut_of f holds
rng (PairF g) c= rng (PairF f)
let f, g be FinSequence of X; :: thesis: ( g is_Shortcut_of f implies rng (PairF g) c= rng (PairF f) )
assume g is_Shortcut_of f ; :: thesis: rng (PairF g) c= rng (PairF 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
A1: ( Seq fc = sc & Seq fvs = g & g1 = g & g1 is_oriented_vertex_seq_of sc ) by Def3;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (PairF g) or y in rng (PairF f) )
assume y in rng (PairF g) ; :: thesis: y in rng (PairF f)
then consider x being set such that
A2: ( x in dom (PairF g) & y = (PairF g) . x ) by FUNCT_1:def 5;
A3: x in Seg (len (PairF g)) by A2, FINSEQ_1:def 3;
reconsider n = x as Element of NAT by A2;
A4: ( 1 <= n & n <= len (PairF g) ) by A3, FINSEQ_1:3;
A5: len (PairF g) = (len g) -' 1 by Def2;
1 <= len (PairF g) by A4, XXREAL_0:2;
then A6: (len g) -' 1 = (len g) - 1 by A5, NAT_D:39;
len g < (len g) + 1 by NAT_1:13;
then (len g) - 1 < len g by XREAL_1:21;
then A7: n < len g by A4, A5, A6, XXREAL_0:2;
then A8: (PairF g) . x = [(g . n),(g . (n + 1))] by A4, Def2;
A9: n + 1 <= len g by A7, NAT_1:13;
A10: fc * (Sgm (dom fc)) = sc by A1, FINSEQ_1:def 14;
rng (Sgm (dom fc)) = dom fc by FINSEQ_1:71;
then rng fc = rng sc by A10, RELAT_1:47;
then A11: rng sc c= rng (PairF f) by RELAT_1:25;
n + 1 <= (len sc) + 1 by A1, A9, GRAPH_4:def 5;
then A12: n <= len sc by XREAL_1:8;
then A13: sc . n orientedly_joins g1 /. n,g1 /. (n + 1) by A1, A4, GRAPH_4:def 5;
n in dom sc by A4, A12, FINSEQ_3:27;
then sc . n in rng sc by FUNCT_1:def 5;
then consider z being set such that
A14: ( z in dom (PairF f) & (PairF f) . z = sc . n ) by A11, FUNCT_1:def 5;
A15: z in Seg (len (PairF f)) by A14, FINSEQ_1:def 3;
reconsider m = z as Element of NAT by A14;
A16: ( 1 <= m & m <= len (PairF f) ) by A15, FINSEQ_1:3;
then A17: ( 1 <= m & m <= (len f) -' 1 ) by Def2;
then 1 <= (len f) -' 1 by XXREAL_0:2;
then A18: (len f) -' 1 = (len f) - 1 by NAT_D:39;
len f < (len f) + 1 by NAT_1:13;
then (len f) - 1 < len f by XREAL_1:21;
then A19: ( 1 <= m & m < len f ) by A17, A18, XXREAL_0:2;
then A20: [(f . m),(f . (m + 1))] = sc . n by A14, Def2;
m in dom f by A19, FINSEQ_3:27;
then A21: f . m in rng f by FUNCT_1:def 5;
A22: 1 < m + 1 by A16, NAT_1:13;
m + 1 <= len f by A19, NAT_1:13;
then m + 1 in dom f by A22, FINSEQ_3:27;
then A23: f . (m + 1) in rng f by FUNCT_1:def 5;
then A24: the Source of (PGraph X) . (f . m),(f . (m + 1)) = f . m by A21, FUNCT_3:def 5;
the Target of (PGraph X) . (f . m),(f . (m + 1)) = f . (m + 1) by A21, A23, FUNCT_3:def 6;
then A25: ( g1 /. n = f . m & g1 /. (n + 1) = f . (m + 1) ) by A13, A20, A24, GRAPH_4:def 1;
( 1 <= n + 1 & n + 1 <= len g1 ) by A1, A4, A7, NAT_1:13;
then ( g . n = f . m & g . (n + 1) = f . (m + 1) ) by A1, A4, A7, A25, FINSEQ_4:24;
hence y in rng (PairF f) by A2, A8, A14, A20, FUNCT_1:def 5; :: thesis: verum