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