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 that
A1: f . 1 <> f . (len f) and
A2: g is_Shortcut_of f ; :: thesis: g is one-to-one
A3: ( f . 1 = g . 1 & f . (len f) = g . (len g) ) by A2;
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
Seq fc = sc and
Seq fvs = g and
A4: g1 = g and
A5: g1 is_oriented_vertex_seq_of sc by A2;
sc is Simple by GRAPH_4:18;
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 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;
then A9: g1 = vs by A5, A6, GRAPH_4:10;
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in K49(g) or not y in K49(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 ; :: thesis: x = y
assume A13: x <> y ; :: thesis: 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:1;
A16: i1 <= len g by A14, FINSEQ_1:1;
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:1;
A19: i2 <= len g by A17, FINSEQ_1:1;