let G be _Graph; :: thesis: for W being Walk of G
for n being Element of NAT holds (W .cut (1,n)) .edgeSeq() c= W .edgeSeq()

let W be Walk of G; :: thesis: for n being Element of NAT holds (W .cut (1,n)) .edgeSeq() c= W .edgeSeq()
let n be Element of NAT ; :: thesis: (W .cut (1,n)) .edgeSeq() c= W .edgeSeq()
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)) .edgeSeq() c= W .edgeSeq()
set f = (W .cut (1,n)) .edgeSeq() ;
now :: thesis: for e being object st e in (W .cut (1,n)) .edgeSeq() holds
e in W .edgeSeq()
let e be object ; :: thesis: ( e in (W .cut (1,n)) .edgeSeq() implies e in W .edgeSeq() )
assume A2: e in (W .cut (1,n)) .edgeSeq() ; :: thesis:
then consider x, y being object such that
A3: e = [x,y] by RELAT_1:def 1;
A4: y = ((W .cut (1,n)) .edgeSeq()) . x by ;
A5: x in dom ((W .cut (1,n)) .edgeSeq()) by ;
then reconsider x = x as Element of NAT ;
A6: x <= len ((W .cut (1,n)) .edgeSeq()) by ;
A7: 2 * x in dom (W .cut (1,n)) by ;
then 2 * x <= len (W .cut (1,n)) by FINSEQ_3:25;
then 2 * x <= n by ;
then A8: 2 * x <= len W by ;
1 <= 2 * x by ;
then 2 * x in dom W by ;
then A9: x in dom () by Lm41;
then A10: x <= len () by FINSEQ_3:25;
1 <= x by ;
then y = (W .cut (1,n)) . (2 * x) by ;
then A11: y = W . (2 * x) by A1, A7, Lm23;
1 <= x by ;
then (W .edgeSeq()) . x = y by ;
hence e in W .edgeSeq() by ; :: thesis: verum
end;
hence (W .cut (1,n)) .edgeSeq() c= W .edgeSeq() 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)) .edgeSeq() c= W .edgeSeq()
end;
end;