let X be non empty set ; for f, g being FinSequence of X st f . 1 <> f . (len f) & g is_Shortcut_of f holds
g is one-to-one
let f, g be FinSequence of X; ( f . 1 <> f . (len f) & g is_Shortcut_of f implies g is one-to-one )
assume that
A1:
f . 1 <> f . (len f)
and
A2:
g is_Shortcut_of f
; g is one-to-one
A3:
( f . 1 = g . 1 & f . (len f) = g . (len g) )
by A2, Def3;
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
Seq fc = sc
and
Seq fvs = g
and
A4:
g1 = g
and
A5:
g1 is_oriented_vertex_seq_of sc
by A2, Def3;
sc is Simple
by GRAPH_4:20;
then consider vs being FinSequence of the carrier of (PGraph X) such that
A6:
vs is_oriented_vertex_seq_of sc
and
A7:
for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )
by GRAPH_4:def 7;
A8:
len g1 = (len sc) + 1
by A5, GRAPH_4:def 5;
then
1 <= len g1
by NAT_1:11;
then
1 < len g1
by A1, A3, A4, XXREAL_0:1;
then
sc <> {}
by A8, NAT_1:13;
then A9:
g1 = vs
by A5, A6, GRAPH_4:11;
let x, y be set ; FUNCT_1:def 8 ( not x in dom g or not y in dom g or not g . x = g . y or x = y )
assume that
A10:
x in dom g
and
A11:
y in dom g
and
A12:
g . x = g . y
; x = y
assume A13:
x <> y
; contradiction
reconsider i1 = x as Element of NAT by A10;
A14:
x in Seg (len g)
by A10, FINSEQ_1:def 3;
then A15:
1 <= i1
by FINSEQ_1:3;
A16:
i1 <= len g
by A14, FINSEQ_1:3;
reconsider i2 = y as Element of NAT by A11;
A17:
y in Seg (len g)
by A11, FINSEQ_1:def 3;
then A18:
1 <= i2
by FINSEQ_1:3;
A19:
i2 <= len g
by A17, FINSEQ_1:3;
per cases
( i1 <= i2 or i1 > i2 )
;
suppose
i1 <= i2
;
contradictionthen A20:
i1 < i2
by A13, XXREAL_0:1;
then
i1 = 1
by A4, A7, A9, A12, A15, A19;
hence
contradiction
by A1, A3, A4, A7, A9, A12, A19, A20;
verum end; suppose A21:
i1 > i2
;
contradictionthen
i2 = 1
by A4, A7, A9, A12, A16, A18;
hence
contradiction
by A1, A3, A4, A7, A9, A12, A16, A21;
verum end;