let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
for n being Element of NAT holds W1 .vertexAt n = W2 .vertexAt n
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 holds
for n being Element of NAT holds W1 .vertexAt n = W2 .vertexAt n
let W2 be Walk of G2; :: thesis: ( W1 = W2 implies for n being Element of NAT holds W1 .vertexAt n = W2 .vertexAt n )
assume A1: W1 = W2 ; :: thesis: for n being Element of NAT holds W1 .vertexAt n = W2 .vertexAt n
let n be Element of NAT ; :: thesis: W1 .vertexAt n = W2 .vertexAt n

now :: thesis: W1 .vertexAt n = W2 .vertexAt n

per cases ( ( n is odd & n <= len W1 ) or not n is odd or not n <= len W1 ) ;

suppose A2: ( n is odd & n <= len W1 ) ; :: thesis: W1 .vertexAt n = W2 .vertexAt n

hence W1 .vertexAt n = W2 . n by A1, Def8
.= W2 .vertexAt n by A1, A2, Def8 ;
:: thesis: verum

end;

suppose A3: ( not n is odd or not n <= len W1 ) ; :: thesis: W1 .vertexAt n = W2 .vertexAt n

hence W1 .vertexAt n = W1 .first() by Def8
.= W2 .first() by A1
.= W2 .vertexAt n by A1, A3, Def8 ;
:: thesis: verum

end;

end;

end;

hence W1 .vertexAt n = W2 .vertexAt n ; :: thesis: verum