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: 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; :: thesis: verum

end;

hence (W .cut (1,n)) .vertexSeq() c= W .vertexSeq() by TARSKI:def 3; :: thesis: verum

end;

suppose ( not n is odd or not 1 <= n or not n <= len W ) ; :: thesis: (W .cut (1,n)) .vertexSeq() c= W .vertexSeq()

hence (W .cut (1,n)) .vertexSeq() c= W .vertexSeq() by Def11; :: thesis: verum

end;

end;

end;

hence (W .cut (1,n)) .vertexSeq() c= W .vertexSeq() ; :: thesis: verum