theorem Th14: :: GLIB_003:14
for G being WGraph
for x, y, e being set st e Joins x,y,G holds
(G .walkOf (x,e,y)) .weightSeq() = <*((the_Weight_of G) . e)*>