theorem Th16: :: GLIB_003:16

for G being WGraph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq())