let G be simple _Graph; :: thesis: for W1, W2 being Walk of G

for k being odd Nat st k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds

W1 . j = W2 . j ) holds

for j being Nat st 1 <= j & j <= k holds

W1 . j = W2 . j

let W1, W2 be Walk of G; :: thesis: for k being odd Nat st k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds

W1 . j = W2 . j ) holds

for j being Nat st 1 <= j & j <= k holds

W1 . j = W2 . j

let k be odd Nat; :: thesis: ( k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds

W1 . j = W2 . j ) implies for j being Nat st 1 <= j & j <= k holds

W1 . j = W2 . j )

assume that

A1: k <= len W1 and

A2: k <= len W2 and

A3: for j being odd Nat st j <= k holds

W1 . j = W2 . j ; :: thesis: for j being Nat st 1 <= j & j <= k holds

W1 . j = W2 . j

let j be Nat; :: thesis: ( 1 <= j & j <= k implies W1 . j = W2 . j )

assume that

A4: 1 <= j and

A5: j <= k ; :: thesis: W1 . j = W2 . j

for k being odd Nat st k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds

W1 . j = W2 . j ) holds

for j being Nat st 1 <= j & j <= k holds

W1 . j = W2 . j

let W1, W2 be Walk of G; :: thesis: for k being odd Nat st k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds

W1 . j = W2 . j ) holds

for j being Nat st 1 <= j & j <= k holds

W1 . j = W2 . j

let k be odd Nat; :: thesis: ( k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds

W1 . j = W2 . j ) implies for j being Nat st 1 <= j & j <= k holds

W1 . j = W2 . j )

assume that

A1: k <= len W1 and

A2: k <= len W2 and

A3: for j being odd Nat st j <= k holds

W1 . j = W2 . j ; :: thesis: for j being Nat st 1 <= j & j <= k holds

W1 . j = W2 . j

let j be Nat; :: thesis: ( 1 <= j & j <= k implies W1 . j = W2 . j )

assume that

A4: 1 <= j and

A5: j <= k ; :: thesis: W1 . j = W2 . j

per cases
( j is odd or j is even )
;

end;

suppose
j is even
; :: thesis: W1 . j = W2 . j

then reconsider j9 = j as even Nat ;

1 - 1 <= j - 1 by A4, XREAL_1:9;

then reconsider j1 = j9 - 1 as odd Element of NAT by INT_1:3;

A6: j1 < j by XREAL_1:44;

j <= len W1 by A1, A5, XXREAL_0:2;

then j1 < len W1 by A6, XXREAL_0:2;

then A7: W1 . (j1 + 1) Joins W1 . j1,W1 . (j1 + 2),G by GLIB_001:def 3;

j1 + 1 < k by A5, XXREAL_0:1;

then (j1 + 1) + 1 <= k by NAT_1:13;

then A8: W1 . (j1 + 2) = W2 . (j1 + 2) by A3;

j <= len W2 by A2, A5, XXREAL_0:2;

then j1 < len W2 by A6, XXREAL_0:2;

then A9: W2 . (j1 + 1) Joins W2 . j1,W2 . (j1 + 2),G by GLIB_001:def 3;

W1 . j1 = W2 . j1 by A3, A5, A6, XXREAL_0:2;

hence W1 . j = W2 . j by A7, A9, A8, GLIB_000:def 20; :: thesis: verum

end;1 - 1 <= j - 1 by A4, XREAL_1:9;

then reconsider j1 = j9 - 1 as odd Element of NAT by INT_1:3;

A6: j1 < j by XREAL_1:44;

j <= len W1 by A1, A5, XXREAL_0:2;

then j1 < len W1 by A6, XXREAL_0:2;

then A7: W1 . (j1 + 1) Joins W1 . j1,W1 . (j1 + 2),G by GLIB_001:def 3;

j1 + 1 < k by A5, XXREAL_0:1;

then (j1 + 1) + 1 <= k by NAT_1:13;

then A8: W1 . (j1 + 2) = W2 . (j1 + 2) by A3;

j <= len W2 by A2, A5, XXREAL_0:2;

then j1 < len W2 by A6, XXREAL_0:2;

then A9: W2 . (j1 + 1) Joins W2 . j1,W2 . (j1 + 2),G by GLIB_001:def 3;

W1 . j1 = W2 . j1 by A3, A5, A6, XXREAL_0:2;

hence W1 . j = W2 . j by A7, A9, A8, GLIB_000:def 20; :: thesis: verum