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 () ;
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 () 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 ;
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 ;
case A6: len f > 1 ; :: thesis: f is one-to-one
A7: f1 is_oriented_vertex_seq_of PairF f by ;
then len f1 = (len ()) + 1 by GRAPH_4:def 5;
then 1 - 1 < ((len ()) + 1) - 1 by ;
then PairF f <> {} ;
then A8: vs = f1 by ;
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 ;
A12: dom f = Seg (len f) by FINSEQ_1:def 3;
then A13: i <= len f by ;
A14: j <= len f by ;
A15: 1 <= j by ;
A16: 1 <= i by ;
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 ;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence x = y ; :: thesis: verum
end;
hence f is one-to-one ; :: 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;