:: deftheorem Def18 defines .weightSeq() GLIB_003:def 18 :
for G being WGraph
for W being Walk of G
for b₃ being FinSequence holds
( b₃ = W .weightSeq() iff ( len b₃ = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b₃ holds
b₃ . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) ) );