let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 is Subwalk of W2 holds

for m being even Element of NAT st 1 <= m & m <= len W1 holds

ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n )

let W1, W2 be Walk of G; :: thesis: ( W1 is Subwalk of W2 implies for m being even Element of NAT st 1 <= m & m <= len W1 holds

ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n ) )

assume W1 is Subwalk of W2 ; :: thesis: for m being even Element of NAT st 1 <= m & m <= len W1 holds

ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n )

then A1: ex es being Subset of (W2 .edgeSeq()) st W1 .edgeSeq() = Seq es by Def32;

let m be even Element of NAT ; :: thesis: ( 1 <= m & m <= len W1 implies ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n ) )

assume that

A2: 1 <= m and

A3: m <= len W1 ; :: thesis: ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n )

A4: W1 . m = (W1 .edgeSeq()) . (m div 2) by A2, A3, Lm40;

m div 2 in dom (W1 .edgeSeq()) by A2, A3, Lm40;

then consider ndiv2 being Element of NAT such that

A5: ndiv2 in dom (W2 .edgeSeq()) and

A6: m div 2 <= ndiv2 and

A7: W1 . m = (W2 .edgeSeq()) . ndiv2 by A1, A4, Th3;

A8: ndiv2 <= len (W2 .edgeSeq()) by A5, FINSEQ_3:25;

2 divides m by PEPIN:22;

then A9: 2 * (m div 2) = m by NAT_D:3;

2 * ndiv2 in dom W2 by A5, Lm41;

then A10: 2 * ndiv2 <= len W2 by FINSEQ_3:25;

1 <= ndiv2 by A5, FINSEQ_3:25;

then W1 . m = W2 . (2 * ndiv2) by A7, A8, Def15;

hence ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n ) by A6, A9, A10, XREAL_1:64; :: thesis: verum

for m being even Element of NAT st 1 <= m & m <= len W1 holds

ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n )

let W1, W2 be Walk of G; :: thesis: ( W1 is Subwalk of W2 implies for m being even Element of NAT st 1 <= m & m <= len W1 holds

ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n ) )

assume W1 is Subwalk of W2 ; :: thesis: for m being even Element of NAT st 1 <= m & m <= len W1 holds

ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n )

then A1: ex es being Subset of (W2 .edgeSeq()) st W1 .edgeSeq() = Seq es by Def32;

let m be even Element of NAT ; :: thesis: ( 1 <= m & m <= len W1 implies ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n ) )

assume that

A2: 1 <= m and

A3: m <= len W1 ; :: thesis: ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n )

A4: W1 . m = (W1 .edgeSeq()) . (m div 2) by A2, A3, Lm40;

m div 2 in dom (W1 .edgeSeq()) by A2, A3, Lm40;

then consider ndiv2 being Element of NAT such that

A5: ndiv2 in dom (W2 .edgeSeq()) and

A6: m div 2 <= ndiv2 and

A7: W1 . m = (W2 .edgeSeq()) . ndiv2 by A1, A4, Th3;

A8: ndiv2 <= len (W2 .edgeSeq()) by A5, FINSEQ_3:25;

2 divides m by PEPIN:22;

then A9: 2 * (m div 2) = m by NAT_D:3;

2 * ndiv2 in dom W2 by A5, Lm41;

then A10: 2 * ndiv2 <= len W2 by FINSEQ_3:25;

1 <= ndiv2 by A5, FINSEQ_3:25;

then W1 . m = W2 . (2 * ndiv2) by A7, A8, Def15;

hence ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n ) by A6, A9, A10, XREAL_1:64; :: thesis: verum