let X be non empty set ; 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; ( 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
; ( 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;
( 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
;
( 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;
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; verum