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

( 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;

end;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 ) )end;

hence
( f is one-to-one & len f <> 1 )
by A2; :: thesis: verumper cases
( len f >= 1 or len f < 1 )
;

end;

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

end;

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

hence
f is one-to-one
; :: thesis: verumper cases
( len f > 1 or len f = 1 )
by A5, XXREAL_0:1;

end;

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

end;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

hence
f is one-to-one
; :: thesis: verum
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;

end;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

hence
x = y
; :: thesis: verumassume A17:
i <> j
; :: thesis: contradiction

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

hence
contradiction
; :: thesis: verumend;

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;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