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