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:
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 ())) + 1 = len W2 by
.= (2 * (len ())) + 1 by Def15 ;
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) by
.= () . x by ;
:: thesis: verum
end;
hence W1 .edgeSeq() = W2 .edgeSeq() by FINSEQ_2:9; :: thesis: verum