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 that
A1: f is one-to-one and
A2: len f > 1 ; :: thesis: ( PairF f is Simple & f . 1 <> f . (len f) )
A3: ( 1 in dom f & len f in dom f ) by A2, FINSEQ_3:25;
reconsider f1 = f as FinSequence of the carrier of (PGraph X) ;
A4: for i, j being Nat st 1 <= i & i < j & j <= len f1 & f1 . i = f1 . j holds
( i = 1 & j = len f1 )

proof

let i, j be Nat; :: thesis: ( 1 <= i & i < j & j <= len f1 & f1 . i = f1 . j implies ( i = 1 & j = len f1 ) )
assume that
A5: 1 <= i and
A6: i < j and
A7: j <= len f1 and
A8: f1 . i = f1 . j ; :: thesis: ( i = 1 & j = len f1 )
1 < j by A5, A6, XXREAL_0:2;
then j in Seg (len f) by A7, FINSEQ_1:1;
then A9: j in dom f by FINSEQ_1:def 3;
i < len f by A6, A7, XXREAL_0:2;
then i in Seg (len f) by A5, FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
hence ( i = 1 & j = len f1 ) by A1, A6, A8, A9; :: thesis: verum

end;

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