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;

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;