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;
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 A2, XXREAL_0:1;
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 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 )
per cases ( W1 . m = W2 . naa1 or W1 . m = W2 . (naa1 + 2) ) by A5, A17, GLIB_000:15;
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 A16, A13; :: 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 A13, A18, NAT_1:12; :: 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 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;
end;
end;
hence ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n ) ; :: thesis: verum