let X be non empty set ; :: thesis: for f being FinSequence of X st PairF f is Simple & f . 1 <> f . (len f) holds
( f is one-to-one & len f <> 1 )
let f be FinSequence of X; :: thesis: ( PairF f is Simple & f . 1 <> f . (len f) implies ( f is one-to-one & len f <> 1 ) )
thus ( PairF f is Simple & f . 1 <> f . (len f) implies ( f is one-to-one & len f <> 1 ) ) :: thesis: verum

proof

reconsider f1 = f as FinSequence of the carrier of (PGraph X) ;
assume that
A1: PairF f is Simple and
A2: f . 1 <> f . (len f) ; :: thesis: ( f is one-to-one & len f <> 1 )
consider vs being FinSequence of the carrier of (PGraph X) such that
A3: vs is_oriented_vertex_seq_of PairF f and
A4: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) by A1, GRAPH_4:def 7;

now :: thesis: ( ( len f >= 1 & f is one-to-one ) or ( len f < 1 & f is one-to-one ) )

per cases ( len f >= 1 or len f < 1 ) ;

case A5: len f >= 1 ; :: thesis: f is one-to-one

now :: thesis: ( ( len f > 1 & f is one-to-one ) or ( len f = 1 & f is one-to-one ) )

per cases ( len f > 1 or len f = 1 ) by A5, XXREAL_0:1;

case A6: len f > 1 ; :: thesis: f is one-to-one

A7: f1 is_oriented_vertex_seq_of PairF f by A5, Th7;
then len f1 = (len (PairF f)) + 1 by GRAPH_4:def 5;
then 1 - 1 < ((len (PairF f)) + 1) - 1 by A6, XREAL_1:9;
then PairF f <> {} ;
then A8: vs = f1 by A3, A7, GRAPH_4:10;
for x, y being object st x in dom f & y in dom f & f . x = f . y holds
x = y

proof

let x, y be object ; :: thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y )
assume that
A9: x in dom f and
A10: y in dom f and
A11: f . x = f . y ; :: thesis: x = y
reconsider i = x, j = y as Element of NAT by A9, A10;
A12: dom f = Seg (len f) by FINSEQ_1:def 3;
then A13: i <= len f by A9, FINSEQ_1:1;
A14: j <= len f by A10, A12, FINSEQ_1:1;
A15: 1 <= j by A10, A12, FINSEQ_1:1;
A16: 1 <= i by A9, A12, FINSEQ_1:1;

now :: thesis: not i <> j

assume A17: i <> j ; :: thesis: contradiction

now :: thesis: ( ( i < j & contradiction ) or ( j < i & contradiction ) )

per cases ( i < j or j < i ) by A17, XXREAL_0:1;

case A18: i < j ; :: thesis: contradiction

then i = 1 by A4, A8, A11, A16, A14;
hence contradiction by A2, A4, A8, A11, A14, A18; :: thesis: verum

end;

case A19: j < i ; :: thesis: contradiction

then j = 1 by A4, A8, A11, A13, A15;
hence contradiction by A2, A4, A8, A11, A13, A19; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence x = y ; :: thesis: verum

end;

hence f is one-to-one ; :: thesis: verum

end;

case len f = 1 ; :: thesis: f is one-to-one

hence f is one-to-one by A2; :: thesis: verum

end;

end;

end;

hence f is one-to-one ; :: thesis: verum

end;

case len f < 1 ; :: thesis: f is one-to-one

then (len f) + 1 <= 1 by NAT_1:13;
then ((len f) + 1) - 1 <= 1 - 1 by XREAL_1:9;
then len f = 0 ;
then Seg (len f) = {} ;
then for x, y being object st x in dom f & y in dom f & f . x = f . y holds
x = y by FINSEQ_1:def 3;
hence f is one-to-one ; :: thesis: verum

end;

end;

end;

hence ( f is one-to-one & len f <> 1 ) by A2; :: thesis: verum

end;