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:84;
then len ((G .walkOf x,e,y) .edgeSeq() ) = 1 by FINSEQ_1:56;
then A2: len ((G .walkOf x,e,y) .weightSeq() ) = 1 by Def18;

A3: now

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 by FINSEQ_1:57
.= <*((the_Weight_of G) . e)*> . n by A6, FINSEQ_1:57 ;
:: thesis: verum

end;

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