theorem :: GLIB_001:32

for G being _Graph
for W1, W2 being Walk of G
for n being Element of NAT st n in dom W1 holds
( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) ) by Lm12;