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()

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() end;

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

end;

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() ;

end;now :: thesis: for v being object st v in (W .cut (1,n)) .vertexSeq() holds

v in W .vertexSeq()

hence
(W .cut (1,n)) .vertexSeq() c= W .vertexSeq()
by TARSKI:def 3; :: thesis: verumv 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;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

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

end;

end;