let X be non empty set ; :: thesis: 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; :: thesis: ( f . 1 <> f . (len f) & g is_Shortcut_of f implies g is one-to-one )
assume A1:
( f . 1 <> f . (len f) & g is_Shortcut_of f )
; :: thesis: g is one-to-one
then A2:
( f . 1 = g . 1 & f . (len f) = g . (len g) & ex fc being Subset of (PairF f) ex fvs being Subset of f ex sc being oriented simple Chain of PGraph X ex g1 being FinSequence of the carrier of (PGraph X) st
( Seq fc = sc & Seq fvs = g & g1 = g & g1 is_oriented_vertex_seq_of sc ) )
by Def3;
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 & Seq fvs = g & g1 = g & g1 is_oriented_vertex_seq_of sc )
by A1, Def3;
sc is Simple
by GRAPH_4:20;
then consider vs being FinSequence of the carrier of (PGraph X) such that
A4:
( vs is_oriented_vertex_seq_of sc & ( 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;
A5:
( len g1 = (len sc) + 1 & ( for n being Element of NAT st 1 <= n & n <= len sc holds
sc . n orientedly_joins g1 /. n,g1 /. (n + 1) ) )
by A3, GRAPH_4:def 5;
then
1 <= len g1
by NAT_1:11;
then
1 < len g1
by A1, A2, A3, XXREAL_0:1;
then
len sc >= 1
by A5, NAT_1:13;
then
sc <> {}
;
then A6:
g1 = vs
by A3, A4, GRAPH_4:11;
let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in dom g or not y in dom g or not g . x = g . y or x = y )
assume A7:
( x in dom g & y in dom g & g . x = g . y )
; :: thesis: x = y
then A8:
x in Seg (len g)
by FINSEQ_1:def 3;
reconsider i1 = x as Element of NAT by A7;
A9:
y in Seg (len g)
by A7, FINSEQ_1:def 3;
reconsider i2 = y as Element of NAT by A7;
A10:
( 1 <= i1 & i1 <= len g )
by A8, FINSEQ_1:3;
A11:
( 1 <= i2 & i2 <= len g )
by A9, FINSEQ_1:3;
assume A12:
x <> y
; :: thesis: contradiction