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

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

end;

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

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

e in W .edgeSeq()

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

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 A2, A3, FUNCT_1:1;

A5: x in dom ((W .cut (1,n)) .edgeSeq()) by A2, A3, FUNCT_1:1;

then reconsider x = x as Element of NAT ;

A6: x <= len ((W .cut (1,n)) .edgeSeq()) by A5, FINSEQ_3:25;

A7: 2 * x in dom (W .cut (1,n)) by A5, Lm41;

then 2 * x <= len (W .cut (1,n)) by FINSEQ_3:25;

then 2 * x <= n by A1, Lm22;

then A8: 2 * x <= len W by A1, XXREAL_0:2;

1 <= 2 * x by A7, FINSEQ_3:25;

then 2 * x in dom W by A8, FINSEQ_3:25;

then A9: x in dom (W .edgeSeq()) by Lm41;

then A10: x <= len (W .edgeSeq()) by FINSEQ_3:25;

1 <= x by A5, FINSEQ_3:25;

then y = (W .cut (1,n)) . (2 * x) by A4, A6, Def15;

then A11: y = W . (2 * x) by A1, A7, Lm23;

1 <= x by A9, FINSEQ_3:25;

then (W .edgeSeq()) . x = y by A11, A10, Def15;

hence e in W .edgeSeq() by A3, A9, FUNCT_1:1; :: thesis: verum

end;assume A2: e in (W .cut (1,n)) .edgeSeq() ; :: thesis: e in W .edgeSeq()

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 A2, A3, FUNCT_1:1;

A5: x in dom ((W .cut (1,n)) .edgeSeq()) by A2, A3, FUNCT_1:1;

then reconsider x = x as Element of NAT ;

A6: x <= len ((W .cut (1,n)) .edgeSeq()) by A5, FINSEQ_3:25;

A7: 2 * x in dom (W .cut (1,n)) by A5, Lm41;

then 2 * x <= len (W .cut (1,n)) by FINSEQ_3:25;

then 2 * x <= n by A1, Lm22;

then A8: 2 * x <= len W by A1, XXREAL_0:2;

1 <= 2 * x by A7, FINSEQ_3:25;

then 2 * x in dom W by A8, FINSEQ_3:25;

then A9: x in dom (W .edgeSeq()) by Lm41;

then A10: x <= len (W .edgeSeq()) by FINSEQ_3:25;

1 <= x by A5, FINSEQ_3:25;

then y = (W .cut (1,n)) . (2 * x) by A4, A6, Def15;

then A11: y = W . (2 * x) by A1, A7, Lm23;

1 <= x by A9, FINSEQ_3:25;

then (W .edgeSeq()) . x = y by A11, A10, Def15;

hence e in W .edgeSeq() 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)) .edgeSeq() c= W .edgeSeq()

end;

end;