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) )

A1: len (PairF g) = (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 (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

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 A3, FINSEQ_1:def 14;

then rng fc = rng sc by A6, RELAT_1:28;

then A7: rng sc c= rng (PairF f) 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 (PairF g) or y in rng (PairF f) )

assume y in rng (PairF g) ; :: thesis: y in rng (PairF f)

then consider x being object such that

A9: x in dom (PairF g) and

A10: y = (PairF g) . x by FUNCT_1:def 3;

reconsider n = x as Element of NAT by A9;

A11: x in Seg (len (PairF g)) by A9, FINSEQ_1:def 3;

then A12: 1 <= n by FINSEQ_1:1;

then A13: 1 <= n + 1 by NAT_1:13;

A14: n <= len (PairF g) by A11, FINSEQ_1:1;

then 1 <= len (PairF g) by A12, XXREAL_0:2;

then (len g) -' 1 = (len g) - 1 by A1, NAT_D:39;

then A15: n < len g by A14, A1, A2, XXREAL_0:2;

then n + 1 <= len g by NAT_1:13;

then n + 1 <= (len sc) + 1 by A4, A5, GRAPH_4:def 5;

then A16: n <= len sc by XREAL_1:6;

then A17: sc . n orientedly_joins g1 /. n,g1 /. (n + 1) by A5, A12, GRAPH_4:def 5;

n in dom sc by A12, A16, FINSEQ_3:25;

then sc . n in rng sc by FUNCT_1:def 3;

then consider z being object such that

A18: z in dom (PairF f) and

A19: (PairF f) . z = sc . n by A7, FUNCT_1:def 3;

reconsider m = z as Element of NAT by A18;

A20: z in Seg (len (PairF f)) by A18, FINSEQ_1:def 3;

then A21: 1 <= m by FINSEQ_1:1;

m <= len (PairF f) by A20, FINSEQ_1:1;

then A22: m <= (len f) -' 1 by Def2;

then 1 <= (len f) -' 1 by A21, XXREAL_0:2;

then (len f) -' 1 = (len f) - 1 by NAT_D:39;

then A23: m < len f by A22, A8, XXREAL_0:2;

then A24: m + 1 <= len f by NAT_1:13;

A25: 1 <= m by A20, FINSEQ_1:1;

then A26: [(f . m),(f . (m + 1))] = sc . n by A19, A23, Def2;

1 < m + 1 by A21, NAT_1:13;

then m + 1 in dom f by A24, FINSEQ_3:25;

then A27: f . (m + 1) in rng f by FUNCT_1:def 3;

m in dom f by A25, A23, FINSEQ_3:25;

then A28: f . m in rng f by FUNCT_1:def 3;

then the Source of (PGraph X) . ((f . m),(f . (m + 1))) = f . m by A27, FUNCT_3:def 4;

then g1 /. n = f . m by A17, A26, GRAPH_4:def 1;

then A29: g . n = f . m by A4, A12, A15, FINSEQ_4:15;

A30: (PairF g) . x = [(g . n),(g . (n + 1))] by A12, A15, Def2;

the Target of (PGraph X) . ((f . m),(f . (m + 1))) = f . (m + 1) by A28, A27, FUNCT_3:def 5;

then A31: g1 /. (n + 1) = f . (m + 1) by A17, A26, GRAPH_4:def 1;

n + 1 <= len g1 by A4, A15, NAT_1:13;

then g . (n + 1) = f . (m + 1) by A4, A31, A13, FINSEQ_4:15;

hence y in rng (PairF f) by A10, A30, A18, A19, A26, A29, FUNCT_1:def 3; :: thesis: verum

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) )

A1: len (PairF g) = (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 (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

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 A3, FINSEQ_1:def 14;

then rng fc = rng sc by A6, RELAT_1:28;

then A7: rng sc c= rng (PairF f) 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 (PairF g) or y in rng (PairF f) )

assume y in rng (PairF g) ; :: thesis: y in rng (PairF f)

then consider x being object such that

A9: x in dom (PairF g) and

A10: y = (PairF g) . x by FUNCT_1:def 3;

reconsider n = x as Element of NAT by A9;

A11: x in Seg (len (PairF g)) by A9, FINSEQ_1:def 3;

then A12: 1 <= n by FINSEQ_1:1;

then A13: 1 <= n + 1 by NAT_1:13;

A14: n <= len (PairF g) by A11, FINSEQ_1:1;

then 1 <= len (PairF g) by A12, XXREAL_0:2;

then (len g) -' 1 = (len g) - 1 by A1, NAT_D:39;

then A15: n < len g by A14, A1, A2, XXREAL_0:2;

then n + 1 <= len g by NAT_1:13;

then n + 1 <= (len sc) + 1 by A4, A5, GRAPH_4:def 5;

then A16: n <= len sc by XREAL_1:6;

then A17: sc . n orientedly_joins g1 /. n,g1 /. (n + 1) by A5, A12, GRAPH_4:def 5;

n in dom sc by A12, A16, FINSEQ_3:25;

then sc . n in rng sc by FUNCT_1:def 3;

then consider z being object such that

A18: z in dom (PairF f) and

A19: (PairF f) . z = sc . n by A7, FUNCT_1:def 3;

reconsider m = z as Element of NAT by A18;

A20: z in Seg (len (PairF f)) by A18, FINSEQ_1:def 3;

then A21: 1 <= m by FINSEQ_1:1;

m <= len (PairF f) by A20, FINSEQ_1:1;

then A22: m <= (len f) -' 1 by Def2;

then 1 <= (len f) -' 1 by A21, XXREAL_0:2;

then (len f) -' 1 = (len f) - 1 by NAT_D:39;

then A23: m < len f by A22, A8, XXREAL_0:2;

then A24: m + 1 <= len f by NAT_1:13;

A25: 1 <= m by A20, FINSEQ_1:1;

then A26: [(f . m),(f . (m + 1))] = sc . n by A19, A23, Def2;

1 < m + 1 by A21, NAT_1:13;

then m + 1 in dom f by A24, FINSEQ_3:25;

then A27: f . (m + 1) in rng f by FUNCT_1:def 3;

m in dom f by A25, A23, FINSEQ_3:25;

then A28: f . m in rng f by FUNCT_1:def 3;

then the Source of (PGraph X) . ((f . m),(f . (m + 1))) = f . m by A27, FUNCT_3:def 4;

then g1 /. n = f . m by A17, A26, GRAPH_4:def 1;

then A29: g . n = f . m by A4, A12, A15, FINSEQ_4:15;

A30: (PairF g) . x = [(g . n),(g . (n + 1))] by A12, A15, Def2;

the Target of (PGraph X) . ((f . m),(f . (m + 1))) = f . (m + 1) by A28, A27, FUNCT_3:def 5;

then A31: g1 /. (n + 1) = f . (m + 1) by A17, A26, GRAPH_4:def 1;

n + 1 <= len g1 by A4, A15, NAT_1:13;

then g . (n + 1) = f . (m + 1) by A4, A31, A13, FINSEQ_4:15;

hence y in rng (PairF f) by A10, A30, A18, A19, A26, A29, FUNCT_1:def 3; :: thesis: verum