let X be non empty set ; :: thesis: for f being FinSequence of X st f is one-to-one & len f > 1 holds
( PairF f is Simple & f . 1 <> f . (len f) )
let f be FinSequence of X; :: thesis: ( f is one-to-one & len f > 1 implies ( PairF f is Simple & f . 1 <> f . (len f) ) )
assume A1: ( f is one-to-one & len f > 1 ) ; :: thesis: ( PairF f is Simple & f . 1 <> f . (len f) )
then A2: 1 in dom f by FINSEQ_3:27;
A3: len f in dom f by A1, FINSEQ_3:27;
reconsider f1 = f as FinSequence of the carrier of (PGraph X) ;
A4: f1 is_oriented_vertex_seq_of PairF f by A1, Th11;
for i, j being Element of NAT st 1 <= i & i < j & j <= len f1 & f1 . i = f1 . j holds
( i = 1 & j = len f1 )

proof

let i, j be Element of NAT ; :: thesis: ( 1 <= i & i < j & j <= len f1 & f1 . i = f1 . j implies ( i = 1 & j = len f1 ) )
assume A5: ( 1 <= i & i < j & j <= len f1 & f1 . i = f1 . j ) ; :: thesis: ( i = 1 & j = len f1 )
then A6: i < len f by XXREAL_0:2;
1 < j by A5, XXREAL_0:2;
then A7: j in Seg (len f) by A5, FINSEQ_1:3;
i in Seg (len f) by A5, A6, FINSEQ_1:3;
then ( i in dom f & j in dom f ) by A7, FINSEQ_1:def 3;
hence ( i = 1 & j = len f1 ) by A1, A5, FUNCT_1:def 8; :: thesis: verum

end;

hence ( PairF f is Simple & f . 1 <> f . (len f) ) by A1, A2, A3, A4, FUNCT_1:def 8, GRAPH_4:def 7; :: thesis: verum