let X be non empty set ; 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; ( 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 ) )
verumproof
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)
;
( 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 ( ( 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
;
f is one-to-one now ( ( 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 A5, XXREAL_0:1;
case A6:
len f > 1
;
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
proof
let x,
y be
object ;
( 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
;
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 not i <> jassume A17:
i <> j
;
contradictionnow ( ( i < j & contradiction ) or ( j < i & contradiction ) )end; hence
contradiction
;
verum end;
hence
x = y
;
verum
end; hence
f is
one-to-one
;
verum end; end; end; hence
f is
one-to-one
;
verum end; end; end;
hence
(
f is
one-to-one &
len f <> 1 )
by A2;
verum
end;