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

assume A1: ( PairF f is Simple & f . 1 <> f . (len f) ) ; :: thesis: ( f is one-to-one & len f <> 1 )
then consider vs being FinSequence of the carrier of (PGraph X) such that
A2: ( vs is_oriented_vertex_seq_of PairF f & ( 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;
reconsider f1 = f as FinSequence of the carrier of (PGraph X) ;

now

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

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

now

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

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

A5: f1 is_oriented_vertex_seq_of PairF f by A3, Th11;
then len f1 = (len (PairF f)) + 1 by GRAPH_4:def 5;
then 1 - 1 < ((len (PairF f)) + 1) - 1 by A4, XREAL_1:11;
then PairF f <> {} ;
then A6: vs = f1 by A2, A5, GRAPH_4:11;
for x, y being set st x in dom f & y in dom f & f . x = f . y holds
x = y

proof

let x, y be set ; :: thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y )
assume A7: ( x in dom f & y in dom f & f . x = f . y ) ; :: thesis: x = y
A8: dom f = Seg (len f) by FINSEQ_1:def 3;
reconsider i = x, j = y as Element of NAT by A7;
A9: ( 1 <= i & i <= len f ) by A7, A8, FINSEQ_1:3;
A10: ( 1 <= j & j <= len f ) by A7, A8, FINSEQ_1:3;

now

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

now

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

case i < j ; :: thesis: contradiction

then ( i = 1 & j = len f ) by A2, A6, A7, A9, A10;
hence contradiction by A1, A7; :: thesis: verum

end;

case j < i ; :: thesis: contradiction

then ( j = 1 & i = len f ) by A2, A6, A7, A9, A10;
hence contradiction by A1, A7; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence x = y ; :: thesis: verum

end;

hence f is one-to-one by FUNCT_1:def 8; :: thesis: verum

end;

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

hence f is one-to-one by A1; :: 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:11;
then len f = 0 ;
then for x, y being set st x in dom f & y in dom f & f . x = f . y holds
x = y by FINSEQ_1:4, FINSEQ_1:def 3;
hence f is one-to-one by FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

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

end;