let G be simple _Graph; 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; 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; ( 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
; for j being Nat st 1 <= j & j <= k holds
W1 . j = W2 . j
let j be Nat; ( 1 <= j & j <= k implies W1 . j = W2 . j )
assume that
A4:
1 <= j
and
A5:
j <= k
; W1 . j = W2 . j
per cases
( j is odd or j is even )
;
suppose
j is
even
;
W1 . j = W2 . jthen 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;
verum end; end;