let G1, G2 be WGraph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & the_Weight_of G1 = the_Weight_of G2 holds
W1 .weightSeq() = W2 .weightSeq()
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 & the_Weight_of G1 = the_Weight_of G2 holds
W1 .weightSeq() = W2 .weightSeq()
let W2 be Walk of G2; :: thesis: ( W1 = W2 & the_Weight_of G1 = the_Weight_of G2 implies W1 .weightSeq() = W2 .weightSeq() )
assume A1: ( W1 = W2 & the_Weight_of G1 = the_Weight_of G2 ) ; :: thesis: W1 .weightSeq() = W2 .weightSeq()
then A2: W1 .edgeSeq() = W2 .edgeSeq() by GLIB_001:87;
set WS1 = W1 .weightSeq() ;
set WS2 = W2 .weightSeq() ;

now

thus len (W1 .weightSeq() ) = len (W1 .weightSeq() ) ; :: thesis: ( len (W2 .weightSeq() ) = len (W1 .weightSeq() ) & ( for x being Nat st x in dom (W1 .weightSeq() ) holds
(W2 .weightSeq() ) . x = (W1 .weightSeq() ) . x ) )
thus A3: len (W2 .weightSeq() ) = len (W1 .edgeSeq() ) by A2, Def18
.= len (W1 .weightSeq() ) by Def18 ; :: thesis: for x being Nat st x in dom (W1 .weightSeq() ) holds
(W2 .weightSeq() ) . x = (W1 .weightSeq() ) . x
let x be Nat; :: thesis: ( x in dom (W1 .weightSeq() ) implies (W2 .weightSeq() ) . x = (W1 .weightSeq() ) . x )
assume x in dom (W1 .weightSeq() ) ; :: thesis: (W2 .weightSeq() ) . x = (W1 .weightSeq() ) . x
then A4: ( 1 <= x & x <= len (W1 .weightSeq() ) & x <= len (W2 .weightSeq() ) ) by A3, FINSEQ_3:27;
hence (W2 .weightSeq() ) . x = (the_Weight_of G2) . ((W2 .edgeSeq() ) . x) by Def18
.= (the_Weight_of G1) . ((W1 .edgeSeq() ) . x) by A1, GLIB_001:87
.= (W1 .weightSeq() ) . x by A4, Def18 ;
:: thesis: verum

end;

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