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()

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 :: thesis: ( len (W1 .edgeSeq()) = len (W1 .edgeSeq()) & len (W2 .edgeSeq()) = len (W1 .edgeSeq()) & ( for x being Nat st x in dom (W1 .edgeSeq()) holds

(W1 .edgeSeq()) . x = (W2 .edgeSeq()) . x ) )

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

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 A3: x in dom (W1 .edgeSeq()) ; :: thesis: (W1 .edgeSeq()) . x = (W2 .edgeSeq()) . x

then A4: x <= len (W2 .edgeSeq()) by A2, FINSEQ_3:25;

A5: 1 <= x by A3, FINSEQ_3:25;

x <= len (W1 .edgeSeq()) by A3, FINSEQ_3:25;

hence (W1 .edgeSeq()) . x = W2 . (2 * x) by A1, A5, Def15

.= (W2 .edgeSeq()) . x by A5, A4, Def15 ;

:: thesis: verum

end;(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 A3: x in dom (W1 .edgeSeq()) ; :: thesis: (W1 .edgeSeq()) . x = (W2 .edgeSeq()) . x

then A4: x <= len (W2 .edgeSeq()) by A2, FINSEQ_3:25;

A5: 1 <= x by A3, FINSEQ_3:25;

x <= len (W1 .edgeSeq()) by A3, FINSEQ_3:25;

hence (W1 .edgeSeq()) . x = W2 . (2 * x) by A1, A5, Def15

.= (W2 .edgeSeq()) . x by A5, A4, Def15 ;

:: thesis: verum