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 (W2 .edgeSeq()) st W1 .edgeSeq() = Seq es by A1, Def32;

( m <= n & n <= len W2 & W1 . m = W2 . n ) ; :: thesis: verum

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 (W2 .edgeSeq()) st W1 .edgeSeq() = Seq es by A1, Def32;

now :: thesis: ex n being odd Element of NAT st

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

hence
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 A2, XXREAL_0:1;

end;

suppose A4:
m < len W1
; :: thesis: ex n being odd Element of NAT st

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

( 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 A4, NAT_1:13;

then A8: W1 . m1 = (W1 .edgeSeq()) . (m1 div 2) by A6, Lm40;

m1 div 2 in dom (W1 .edgeSeq()) by A6, A7, Lm40;

then consider x being Element of NAT such that

A9: x in dom (W2 .edgeSeq()) and

A10: m1 div 2 <= x and

A11: W1 . m1 = (W2 .edgeSeq()) . x by A3, A8, Th3;

set n = 2 * x;

A12: 1 <= x by A9, FINSEQ_3:25;

2 divides m1 by PEPIN:22;

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

then m1 <= 2 * x by A10, XREAL_1:64;

then A13: m1 - 1 <= (2 * x) - 1 by XREAL_1:13;

A14: x <= len (W2 .edgeSeq()) by A9, FINSEQ_3:25;

A15: 2 * x in dom W2 by A9, Lm41;

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 A15, FINSEQ_3:25;

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 A11, A12, A14, Def15;

A18: naa1 + 2 <= len W2 by A16, Th1;

( m <= n & n <= len W2 & W1 . m = W2 . n ) ; :: thesis: verum

end;reconsider m1 = m + 1 as even Element of NAT ;

A6: 1 <= m1 by NAT_1:12;

A7: m1 <= len W1 by A4, NAT_1:13;

then A8: W1 . m1 = (W1 .edgeSeq()) . (m1 div 2) by A6, Lm40;

m1 div 2 in dom (W1 .edgeSeq()) by A6, A7, Lm40;

then consider x being Element of NAT such that

A9: x in dom (W2 .edgeSeq()) and

A10: m1 div 2 <= x and

A11: W1 . m1 = (W2 .edgeSeq()) . x by A3, A8, Th3;

set n = 2 * x;

A12: 1 <= x by A9, FINSEQ_3:25;

2 divides m1 by PEPIN:22;

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

then m1 <= 2 * x by A10, XREAL_1:64;

then A13: m1 - 1 <= (2 * x) - 1 by XREAL_1:13;

A14: x <= len (W2 .edgeSeq()) by A9, FINSEQ_3:25;

A15: 2 * x in dom W2 by A9, Lm41;

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 A15, FINSEQ_3:25;

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 A11, A12, A14, Def15;

A18: naa1 + 2 <= len W2 by A16, Th1;

now :: thesis: ex n being odd Element of NAT st

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

hence
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 A5, A17, GLIB_000:15;

end;

( m <= n & n <= len W2 & W1 . m = W2 . n ) ; :: thesis: verum

suppose A19:
m = len W1
; :: thesis: ex n being odd Element of NAT st

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

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

len W1 <= len W2
by A1, Lm72;

then A20: m <= len W2 by A2, XXREAL_0:2;

W1 . m = W1 .last() by A19

.= W2 .last() by A1, Th159

.= 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;then A20: m <= len W2 by A2, XXREAL_0:2;

W1 . m = W1 .last() by A19

.= W2 .last() by A1, Th159

.= 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

( m <= n & n <= len W2 & W1 . m = W2 . n ) ; :: thesis: verum