let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
for m being odd Element of NAT st m <= len W1 holds
ex n being odd 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 odd Element of NAT st m <= len W1 holds
ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n ) )

assume A1: W1 is Subwalk of W2 ; :: thesis: for m being odd Element of NAT st m <= len W1 holds
ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n )

let m be odd Element of NAT ; :: thesis: ( m <= len W1 implies ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n ) )

assume A2: m <= len W1 ; :: thesis: ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n )

A3: ex es being Subset of () st W1 .edgeSeq() = Seq es by ;
now :: thesis: ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n )
per cases ( m < len W1 or m = len W1 ) by ;
suppose A4: m < len W1 ; :: thesis: ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n )

then A5: W1 . (m + 1) Joins W1 . m,W1 . (m + 2),G by Def3;
reconsider m1 = m + 1 as even Element of NAT ;
A6: 1 <= m1 by NAT_1:12;
A7: m1 <= len W1 by ;
then A8: W1 . m1 = () . (m1 div 2) by ;
m1 div 2 in dom () by A6, A7, Lm40;
then consider x being Element of NAT such that
A9: x in dom () and
A10: m1 div 2 <= x and
A11: W1 . m1 = () . x by A3, A8, Th3;
set n = 2 * x;
A12: 1 <= x by ;
2 divides m1 by PEPIN:22;
then 2 * (m1 div 2) = m1 by NAT_D:3;
then m1 <= 2 * x by ;
then A13: m1 - 1 <= (2 * x) - 1 by XREAL_1:13;
A14: x <= len () by ;
A15: 2 * x in dom W2 by ;
then 1 <= 2 * x by FINSEQ_3:25;
then reconsider naa1 = (2 * x) - 1 as odd Element of NAT by INT_1:5;
2 * x <= len W2 by ;
then A16: naa1 < (len W2) - 0 by XREAL_1:15;
then W2 . (naa1 + 1) Joins W2 . naa1,W2 . (naa1 + 2),G by Def3;
then A17: W1 . m1 Joins W2 . naa1,W2 . (naa1 + 2),G by ;
A18: naa1 + 2 <= len W2 by ;
now :: thesis: ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n )
per cases ( W1 . m = W2 . naa1 or W1 . m = W2 . (naa1 + 2) ) by ;
suppose W1 . m = W2 . naa1 ; :: thesis: ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n )

hence ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n ) by ; :: thesis: verum
end;
suppose W1 . m = W2 . (naa1 + 2) ; :: thesis: ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n )

hence ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n ) by ; :: thesis: verum
end;
end;
end;
hence ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n ) ; :: thesis: verum
end;
suppose A19: m = len W1 ; :: thesis: ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n )

len W1 <= len W2 by ;
then A20: m <= len W2 by ;
W1 . m = W1 .last() by A19
.= W2 .last() by
.= W2 . (len W2) ;
hence ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n ) by A20; :: thesis: verum
end;
end;
end;
hence ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n ) ; :: thesis: verum