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
( ( not n is even & 1 <= n & n <= len W ) or n is even or not 1 <= n or not n <= len W )
;
suppose A1:
( not
n is
even & 1
<= n &
n <= len W )
;
(W .cut 1,n) .edgeSeq() c= W .edgeSeq() set f =
(W .cut 1,n) .edgeSeq() ;
now let e be
set ;
( 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
set such that A3:
e = [x,y]
by RELAT_1:def 1;
A4:
y = ((W .cut 1,n) .edgeSeq() ) . x
by A2, A3, FUNCT_1:8;
A5:
x in dom ((W .cut 1,n) .edgeSeq() )
by A2, A3, FUNCT_1:8;
then reconsider x =
x as
Element of
NAT ;
A6:
x <= len ((W .cut 1,n) .edgeSeq() )
by A5, FINSEQ_3:27;
A7:
2
* x in dom (W .cut 1,n)
by A5, Lm41;
then
2
* x <= len (W .cut 1,n)
by FINSEQ_3:27;
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:27;
then
2
* x in dom W
by A8, FINSEQ_3:27;
then A9:
x in dom (W .edgeSeq() )
by Lm41;
then A10:
x <= len (W .edgeSeq() )
by FINSEQ_3:27;
1
<= x
by A5, FINSEQ_3:27;
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:27;
then
(W .edgeSeq() ) . x = y
by A11, A10, Def15;
hence
e in W .edgeSeq()
by A3, A9, FUNCT_1:8;
verum end; hence
(W .cut 1,n) .edgeSeq() c= W .edgeSeq()
by TARSKI:def 3;
verum end;