let G be 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)*>
let x, y, e be set ; ( 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
; (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 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)*> . nlet n be
Nat;
( 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())
;
((G .walkOf (x,e,y)) .weightSeq()) . n = <*((the_Weight_of G) . e)*> . nA6:
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:40
.=
<*((the_Weight_of G) . e)*> . n
by A6, FINSEQ_1:40
;
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; verum