let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .vertexSeq() = W2 .vertexSeq()

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

let W2 be Walk of G2; :: thesis: ( W1 = W2 implies W1 .vertexSeq() = W2 .vertexSeq() )
set VS1 = W1 .vertexSeq() ;
set VS2 = W2 .vertexSeq() ;
assume A1: W1 = W2 ; :: thesis:
now :: thesis: ( len () = len () & len () = len () & ( for x being Nat st x in dom () holds
() . x = () . x ) )
thus len () = len () ; :: thesis: ( len () = len () & ( for x being Nat st x in dom () holds
() . x = () . x ) )

A2: 2 * (len ()) = (len W2) + 1 by
.= 2 * (len ()) by Def14 ;
hence len () = len () ; :: thesis: for x being Nat st x in dom () holds
() . x = () . x

let x be Nat; :: thesis: ( x in dom () implies () . x = () . x )
assume A3: x in dom () ; :: thesis: () . x = () . x
then A4: x <= len () by ;
A5: 1 <= x by ;
x <= len () by ;
hence () . x = W2 . ((2 * x) - 1) by
.= () . x by ;
:: thesis: verum
end;
hence W1 .vertexSeq() = W2 .vertexSeq() by FINSEQ_2:9; :: thesis: verum