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 () 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 = () . (m div 2) by A2, A3, Lm40;
m div 2 in dom () by A2, A3, Lm40;
then consider ndiv2 being Element of NAT such that
A5: ndiv2 in dom () and
A6: m div 2 <= ndiv2 and
A7: W1 . m = () . ndiv2 by A1, A4, Th3;
A8: ndiv2 <= len () by ;
2 divides m by PEPIN:22;
then A9: 2 * (m div 2) = m by NAT_D:3;
2 * ndiv2 in dom W2 by ;
then A10: 2 * ndiv2 <= len W2 by FINSEQ_3:25;
1 <= ndiv2 by ;
then W1 . m = W2 . (2 * ndiv2) by ;
hence ex n being even Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n ) by ; :: thesis: verum