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: W1 .vertexSeq() = W2 .vertexSeq()

now :: thesis: ( len (W1 .vertexSeq()) = len (W1 .vertexSeq()) & len (W2 .vertexSeq()) = len (W1 .vertexSeq()) & ( for x being Nat st x in dom (W1 .vertexSeq()) holds
(W1 .vertexSeq()) . x = (W2 .vertexSeq()) . x ) )

thus len (W1 .vertexSeq()) = len (W1 .vertexSeq()) ; :: thesis: ( len (W2 .vertexSeq()) = len (W1 .vertexSeq()) & ( for x being Nat st x in dom (W1 .vertexSeq()) holds
(W1 .vertexSeq()) . x = (W2 .vertexSeq()) . x ) )
A2: 2 * (len (W1 .vertexSeq())) = (len W2) + 1 by A1, Def14
.= 2 * (len (W2 .vertexSeq())) by Def14 ;
hence len (W2 .vertexSeq()) = len (W1 .vertexSeq()) ; :: thesis: for x being Nat st x in dom (W1 .vertexSeq()) holds
(W1 .vertexSeq()) . x = (W2 .vertexSeq()) . x
let x be Nat; :: thesis: ( x in dom (W1 .vertexSeq()) implies (W1 .vertexSeq()) . x = (W2 .vertexSeq()) . x )
assume A3: x in dom (W1 .vertexSeq()) ; :: thesis: (W1 .vertexSeq()) . x = (W2 .vertexSeq()) . x
then A4: x <= len (W2 .vertexSeq()) by A2, FINSEQ_3:25;
A5: 1 <= x by A3, FINSEQ_3:25;
x <= len (W1 .vertexSeq()) by A3, FINSEQ_3:25;
hence (W1 .vertexSeq()) . x = W2 . ((2 * x) - 1) by A1, A5, Def14
.= (W2 .vertexSeq()) . x by A5, A4, Def14 ;
:: thesis: verum

end;

hence W1 .vertexSeq() = W2 .vertexSeq() by FINSEQ_2:9; :: thesis: verum