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 :: thesis: (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 ) ; :: thesis: (W .cut (1,n)) .vertexSeq() c= W .vertexSeq()
set f = (W .cut (1,n)) .vertexSeq() ;
now :: thesis: for v being object st v in (W .cut (1,n)) .vertexSeq() holds
v in W .vertexSeq()
let v be object ; :: thesis: ( v in (W .cut (1,n)) .vertexSeq() implies v in W .vertexSeq() )
assume A2: v in (W .cut (1,n)) .vertexSeq() ; :: thesis:
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 ;
A5: x in dom ((W .cut (1,n)) .vertexSeq()) by ;
then reconsider x = x as Element of NAT ;
A6: x <= len ((W .cut (1,n)) .vertexSeq()) by ;
A7: (2 * x) - 1 in dom (W .cut (1,n)) by ;
then (2 * x) - 1 <= len (W .cut (1,n)) by FINSEQ_3:25;
then (2 * x) - 1 <= n by ;
then A8: (2 * x) - 1 <= len W by ;
1 <= (2 * x) - 1 by ;
then (2 * x) - 1 in dom W by ;
then A9: x in dom () by Th71;
then A10: x <= len () by FINSEQ_3:25;
1 <= x by ;
then y = (W .cut (1,n)) . ((2 * x) - 1) by ;
then A11: y = W . ((2 * x) - 1) by A1, A7, Lm23;
1 <= x by ;
then (W .vertexSeq()) . x = y by ;
hence v in W .vertexSeq() by ; :: thesis: verum
end;
hence (W .cut (1,n)) .vertexSeq() c= W .vertexSeq() by TARSKI:def 3; :: thesis: verum
end;
end;
end;
hence (W .cut (1,n)) .vertexSeq() c= W .vertexSeq() ; :: thesis: verum