let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1

for W2 being Walk of G2

for n being odd Nat st W1 .vertexSeq() = W2 .vertexSeq() holds

W1 . n = W2 . n

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2

for n being odd Nat st W1 .vertexSeq() = W2 .vertexSeq() holds

W1 . n = W2 . n

let W2 be Walk of G2; :: thesis: for n being odd Nat st W1 .vertexSeq() = W2 .vertexSeq() holds

W1 . n = W2 . n

let n be odd Nat; :: thesis: ( W1 .vertexSeq() = W2 .vertexSeq() implies W1 . n = W2 . n )

assume A1: W1 .vertexSeq() = W2 .vertexSeq() ; :: thesis: W1 . n = W2 . n

then A2: len W1 = len W2 by Lm3;

reconsider m = n as odd Element of NAT by ORDINAL1:def 12;

for W2 being Walk of G2

for n being odd Nat st W1 .vertexSeq() = W2 .vertexSeq() holds

W1 . n = W2 . n

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2

for n being odd Nat st W1 .vertexSeq() = W2 .vertexSeq() holds

W1 . n = W2 . n

let W2 be Walk of G2; :: thesis: for n being odd Nat st W1 .vertexSeq() = W2 .vertexSeq() holds

W1 . n = W2 . n

let n be odd Nat; :: thesis: ( W1 .vertexSeq() = W2 .vertexSeq() implies W1 . n = W2 . n )

assume A1: W1 .vertexSeq() = W2 .vertexSeq() ; :: thesis: W1 . n = W2 . n

then A2: len W1 = len W2 by Lm3;

reconsider m = n as odd Element of NAT by ORDINAL1:def 12;

per cases
( n <= len W1 or n > len W1 )
;

end;

suppose A3:
n <= len W1
; :: thesis: W1 . n = W2 . n

hence W1 . n =
W1 .vertexAt n
by GLIB_001:def 8

.= (W2 .vertexSeq()) . ((m + 1) div 2) by A1, A3, GLIB_001:72

.= W2 .vertexAt n by A2, A3, GLIB_001:72

.= W2 . n by A2, A3, GLIB_001:def 8 ;

:: thesis: verum

end;.= (W2 .vertexSeq()) . ((m + 1) div 2) by A1, A3, GLIB_001:72

.= W2 .vertexAt n by A2, A3, GLIB_001:72

.= W2 . n by A2, A3, GLIB_001:def 8 ;

:: thesis: verum