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:21;
assume
g is_Shortcut_of f
; rng (PairF g) c= rng (PairF 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
A3:
Seq fc = sc
and
Seq fvs = g
and
A4:
g1 = g
and
A5:
g1 is_oriented_vertex_seq_of sc
by Def3;
A6:
rng (Sgm (dom fc)) = dom fc
by FINSEQ_1:71;
fc * (Sgm (dom fc)) = sc
by A3, FINSEQ_1:def 14;
then
rng fc = rng sc
by A6, RELAT_1:47;
then A7:
rng sc c= rng (PairF f)
by RELAT_1:25;
len f < (len f) + 1
by NAT_1:13;
then A8:
(len f) - 1 < len f
by XREAL_1:21;
let y be set ; 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 set such that
A9:
x in dom (PairF g)
and
A10:
y = (PairF g) . x
by FUNCT_1:def 5;
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:3;
then A13:
1 <= n + 1
by NAT_1:13;
A14:
n <= len (PairF g)
by A11, FINSEQ_1:3;
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:8;
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:27;
then
sc . n in rng sc
by FUNCT_1:def 5;
then consider z being set such that
A18:
z in dom (PairF f)
and
A19:
(PairF f) . z = sc . n
by A7, FUNCT_1:def 5;
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:3;
m <= len (PairF f)
by A20, FINSEQ_1:3;
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:3;
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:27;
then A27:
f . (m + 1) in rng f
by FUNCT_1:def 5;
m in dom f
by A25, A23, FINSEQ_3:27;
then A28:
f . m in rng f
by FUNCT_1:def 5;
then
the Source of (PGraph X) . (f . m),(f . (m + 1)) = f . m
by A27, FUNCT_3:def 5;
then
g1 /. n = f . m
by A17, A26, GRAPH_4:def 1;
then A29:
g . n = f . m
by A4, A12, A15, FINSEQ_4:24;
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 6;
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:24;
hence
y in rng (PairF f)
by A10, A30, A18, A19, A26, A29, FUNCT_1:def 5; verum