let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .first() = W2 .first() holds
not len (maxPrefix W1,W2) is even
let W1, W2 be Walk of G; :: thesis: ( W1 .first() = W2 .first() implies not len (maxPrefix W1,W2) is even )
assume that
A1: W1 .first() = W2 .first() and
A2: len (maxPrefix W1,W2) is even ; :: thesis: contradiction
set dI = len (maxPrefix W1,W2);
set mP = maxPrefix W1,W2;
A3: 1 <= len (maxPrefix W1,W2) by A1, Th5;
A4: len (maxPrefix W1,W2) <= len W1 by Th3;
A5: len (maxPrefix W1,W2) <= len W2 by Th3;
A6: len (maxPrefix W1,W2) < len W1 by A2, A4, XXREAL_0:1;
A7: len (maxPrefix W1,W2) < len W2 by A2, A5, XXREAL_0:1;
reconsider dIp = (len (maxPrefix W1,W2)) - 1 as odd Element of NAT by A2, A3, INT_1:18;
A8: dIp < len (maxPrefix W1,W2) by XREAL_1:148;
A9: dIp < len W1 by A4, XREAL_1:148, XXREAL_0:2;
A10: len (maxPrefix W1,W2) = dIp + 1 ;
then A11: W1 . (len (maxPrefix W1,W2)) Joins W1 . dIp,W1 . (dIp + 2),G by A9, GLIB_001:def 3;
dIp < len W2 by A5, XREAL_1:148, XXREAL_0:2;
then A12: W2 . (len (maxPrefix W1,W2)) Joins W2 . dIp,W2 . (dIp + 2),G by A10, GLIB_001:def 3;
W1 . (len (maxPrefix W1,W2)) = W2 . (len (maxPrefix W1,W2)) by Th7;
then A13: ( ( W1 . dIp = W2 . dIp & W1 . (dIp + 2) = W2 . (dIp + 2) ) or ( W1 . dIp = W2 . (dIp + 2) & W1 . (dIp + 2) = W2 . dIp ) ) by A11, A12, GLIB_000:18;
set lmP = (maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>;
A14: len ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) = (len (maxPrefix W1,W2)) + 1 by FINSEQ_2:19;
then len ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) <= len W1 by A6, NAT_1:13;
then A15: dom ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) c= dom W1 by FINSEQ_3:32;

now

let x be set ; :: thesis: ( x in dom ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) implies ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) . b₁ = W1 . b₁ )
assume A16: x in dom ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) ; :: thesis: ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) . b₁ = W1 . b₁
x is Element of NAT by A16;
then reconsider n = x as Nat ;
A17: 1 <= n by A16, FINSEQ_3:27;
n <= len ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) by A16, FINSEQ_3:27;
then A18: n <= (len (maxPrefix W1,W2)) + 1 by FINSEQ_2:19;

per cases ( n <= len (maxPrefix W1,W2) or n = (len (maxPrefix W1,W2)) + 1 ) by A18, NAT_1:8;

suppose A19: n <= len (maxPrefix W1,W2) ; :: thesis: ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) . b₁ = W1 . b₁

then n in dom (maxPrefix W1,W2) by A17, FINSEQ_3:27;
hence ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) . x = (maxPrefix W1,W2) . x by FINSEQ_1:def 7
.= W1 . x by A19, Th6 ;
:: thesis: verum

end;

suppose n = (len (maxPrefix W1,W2)) + 1 ; :: thesis: ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) . b₁ = W1 . b₁

hence ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) . x = W1 . x by FINSEQ_1:59; :: thesis: verum

end;

end;

end;

then A20: (maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*> c= W1 by A15, GRFUNC_1:8;
len ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) <= len W2 by A7, A14, NAT_1:13;
then A21: dom ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) c= dom W2 by FINSEQ_3:32;

now

let x be set ; :: thesis: ( x in dom ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) implies ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) . b₁ = W2 . b₁ )
assume A22: x in dom ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) ; :: thesis: ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) . b₁ = W2 . b₁
x is Element of NAT by A22;
then reconsider n = x as Nat ;
A23: 1 <= n by A22, FINSEQ_3:27;
n <= len ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) by A22, FINSEQ_3:27;
then A24: n <= (len (maxPrefix W1,W2)) + 1 by FINSEQ_2:19;

per cases ( n <= len (maxPrefix W1,W2) or n = (len (maxPrefix W1,W2)) + 1 ) by A24, NAT_1:8;

suppose A25: n <= len (maxPrefix W1,W2) ; :: thesis: ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) . b₁ = W2 . b₁

then n in dom (maxPrefix W1,W2) by A23, FINSEQ_3:27;
hence ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) . x = (maxPrefix W1,W2) . x by FINSEQ_1:def 7
.= W2 . x by A25, Th6 ;
:: thesis: verum

end;

suppose A26: n = (len (maxPrefix W1,W2)) + 1 ; :: thesis: ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) . b₁ = W2 . b₁

hence ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) . x = W1 . ((len (maxPrefix W1,W2)) + 1) by FINSEQ_1:59
.= W2 . x by A8, A13, A26, Th7 ;
:: thesis: verum

end;

end;

end;

then (maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*> c= W2 by A21, GRFUNC_1:8;
then (maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*> c= maxPrefix W1,W2 by A20, Def1;
then len ((maxPrefix W1,W2) ^ <*(W1 . ((len (maxPrefix W1,W2)) + 1))*>) <= len (maxPrefix W1,W2) by FINSEQ_1:84;
then (len (maxPrefix W1,W2)) + 1 <= len (maxPrefix W1,W2) by FINSEQ_2:19;
hence contradiction by NAT_1:13; :: thesis: verum