let G be _Graph; :: thesis: for W being Walk of G
for n being Element of NAT holds (W .cut 1,n) .vertexSeq() c= W .vertexSeq()
let W be Walk of G; :: thesis: for n being Element of NAT holds (W .cut 1,n) .vertexSeq() c= W .vertexSeq()
let n be Element of NAT ; :: thesis: (W .cut 1,n) .vertexSeq() c= W .vertexSeq()
now per cases
( ( not n is even & 1 <= n & n <= len W ) or n is even or not 1 <= n or not n <= len W )
;
suppose A1:
( not
n is
even & 1
<= n &
n <= len W )
;
:: thesis: (W .cut 1,n) .vertexSeq() c= W .vertexSeq() set f =
(W .cut 1,n) .vertexSeq() ;
now let v be
set ;
:: thesis: ( v in (W .cut 1,n) .vertexSeq() implies v in W .vertexSeq() )assume A2:
v in (W .cut 1,n) .vertexSeq()
;
:: thesis: v in W .vertexSeq() then consider x,
y being
set such that A3:
v = [x,y]
by RELAT_1:def 1;
A4:
(
x in dom ((W .cut 1,n) .vertexSeq() ) &
y = ((W .cut 1,n) .vertexSeq() ) . x )
by A2, A3, FUNCT_1:8;
then reconsider x =
x as
Element of
NAT ;
( 1
<= x &
x <= len ((W .cut 1,n) .vertexSeq() ) )
by A4, FINSEQ_3:27;
then A5:
y = (W .cut 1,n) . ((2 * x) - 1)
by A4, Def14;
A6:
(2 * x) - 1
in dom (W .cut 1,n)
by A4, Th74;
then A7:
y = W . ((2 * x) - 1)
by A1, A5, Lm23;
A8:
(2 * x) - 1 is
Element of
NAT
by A6;
A9:
( 1
<= (2 * x) - 1 &
(2 * x) - 1
<= len (W .cut 1,n) )
by A6, FINSEQ_3:27;
then
(2 * x) - 1
<= n
by A1, Lm22;
then
(2 * x) - 1
<= len W
by A1, XXREAL_0:2;
then
(2 * x) - 1
in dom W
by A8, A9, FINSEQ_3:27;
then A10:
x in dom (W .vertexSeq() )
by Th74;
then
( 1
<= x &
x <= len (W .vertexSeq() ) )
by FINSEQ_3:27;
then
(W .vertexSeq() ) . x = y
by A7, Def14;
hence
v in W .vertexSeq()
by A3, A10, FUNCT_1:8;
:: thesis: verum end; hence
(W .cut 1,n) .vertexSeq() c= W .vertexSeq()
by TARSKI:def 3;
:: thesis: verum end;
hence
(W .cut 1,n) .vertexSeq() c= W .vertexSeq()
; :: thesis: verum