let X be non empty set ; 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; ( 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
; 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 ; TARSKI:def 3 ( not y in rng (PairF g) or y in rng (PairF f) )
assume
y in rng (PairF g)
; 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; verum