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