theorem :: GLIB_001:28

for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(len (W1 .append W2)) + 1 = (len W1) + (len W2) by Lm9;