let G be _Graph; 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; for n being Element of NAT holds (W .cut (1,n)) .edgeSeq() c= W .edgeSeq()
let n be Element of NAT ; (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 )
;
(W .cut (1,n)) .edgeSeq() c= W .edgeSeq() set f =
(W .cut (1,n)) .edgeSeq() ;
now for e being object st e in (W .cut (1,n)) .edgeSeq() holds
e in W .edgeSeq() let e be
object ;
( e in (W .cut (1,n)) .edgeSeq() implies e in W .edgeSeq() )assume A2:
e in (W .cut (1,n)) .edgeSeq()
;
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;
verum end; hence
(W .cut (1,n)) .edgeSeq() c= W .edgeSeq()
by TARSKI:def 3;
verum end;