let G be WGraph; :: thesis: for x, y, e being set st e Joins x,y,G holds
(G .walkOf (x,e,y)) .weightSeq() = <*((the_Weight_of G) . e)*>
let x, y, e be set ; :: thesis: ( e Joins x,y,G implies (G .walkOf (x,e,y)) .weightSeq() = <*((the_Weight_of G) . e)*> )
set W = G .walkOf (x,e,y);
assume e Joins x,y,G ; :: thesis: (G .walkOf (x,e,y)) .weightSeq() = <*((the_Weight_of G) . e)*>
then A1: (G .walkOf (x,e,y)) .edgeSeq() = <*e*> by GLIB_001:83;
then len ((G .walkOf (x,e,y)) .edgeSeq()) = 1 by FINSEQ_1:39;
then A2: len ((G .walkOf (x,e,y)) .weightSeq()) = 1 by Def18;

A3: now :: thesis: for n being Nat st 1 <= n & n <= len ((G .walkOf (x,e,y)) .weightSeq()) holds
((G .walkOf (x,e,y)) .weightSeq()) . n = <*((the_Weight_of G) . e)*> . n

let n be Nat; :: thesis: ( 1 <= n & n <= len ((G .walkOf (x,e,y)) .weightSeq()) implies ((G .walkOf (x,e,y)) .weightSeq()) . n = <*((the_Weight_of G) . e)*> . n )
assume that
A4: 1 <= n and
A5: n <= len ((G .walkOf (x,e,y)) .weightSeq()) ; :: thesis: ((G .walkOf (x,e,y)) .weightSeq()) . n = <*((the_Weight_of G) . e)*> . n
A6: n = 1 by A2, A4, A5, XXREAL_0:1;
hence ((G .walkOf (x,e,y)) .weightSeq()) . n = (the_Weight_of G) . (<*e*> . 1) by A1, A5, Def18
.= (the_Weight_of G) . e
.= <*((the_Weight_of G) . e)*> . n by A6 ;
:: thesis: verum

end;

len ((G .walkOf (x,e,y)) .weightSeq()) = len <*((the_Weight_of G) . e)*> by A2, FINSEQ_1:39;
hence (G .walkOf (x,e,y)) .weightSeq() = <*((the_Weight_of G) . e)*> by A3, FINSEQ_1:14; :: thesis: verum