theorem :: GLIB_001:82

for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
(W .addEdge e) .edgeSeq() = (W .edgeSeq()) ^ <*e*> by Lm44;