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;

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

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;

suppose n > len W1 ; :: thesis: W1 . n = W2 . n

then ( not n in dom W1 & not n in dom W2 ) by A2, FINSEQ_3:25;
then ( W1 . n = {} & W2 . n = {} ) by FUNCT_1:def 2;
hence W1 . n = W2 . n ; :: thesis: verum

end;

end;