let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .edgeSeq() = W2 .edgeSeq()
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 holds
W1 .edgeSeq() = W2 .edgeSeq()
let W2 be Walk of G2; :: thesis: ( W1 = W2 implies W1 .edgeSeq() = W2 .edgeSeq() )
set ES1 = W1 .edgeSeq() ;
set ES2 = W2 .edgeSeq() ;
assume A1: W1 = W2 ; :: thesis: W1 .edgeSeq() = W2 .edgeSeq()

now

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

end;

hence W1 .edgeSeq() = W2 .edgeSeq() by FINSEQ_2:10; :: thesis: verum