theorem :: GLIB_003:13

for G being WGraph
for W being Walk of G holds len (W .weightSeq()) = W .length()