for G being nonnegative-weighted WGraph
for W being Walk of G
for n being Element of NAT st n in dom (W .weightSeq()) holds
0 <= (W .weightSeq()) . n