let G be nonnegative-weighted WGraph; :: thesis: for W being Walk of G
for n being Element of NAT st n in dom (W .weightSeq()) holds
0 <= (W .weightSeq()) . n
let W be Walk of G; :: thesis: for n being Element of NAT st n in dom (W .weightSeq()) holds
0 <= (W .weightSeq()) . n
let n be Element of NAT ; :: thesis: ( n in dom (W .weightSeq()) implies 0 <= (W .weightSeq()) . n )
set WS = W .weightSeq() ;
assume A1: n in dom (W .weightSeq()) ; :: thesis: 0 <= (W .weightSeq()) . n
then A2: 1 <= n by FINSEQ_3:25;
A3: n <= len (W .weightSeq()) by A1, FINSEQ_3:25;
then n <= len (W .edgeSeq()) by Def18;
then ( dom (the_Weight_of G) = the_Edges_of G & n in dom (W .edgeSeq()) ) by A2, FINSEQ_3:25, PARTFUN1:def 2;
then A4: (W .edgeSeq()) . n in dom (the_Weight_of G) by GLIB_001:79;
(W .weightSeq()) . n = (the_Weight_of G) . ((W .edgeSeq()) . n) by A2, A3, Def18;
then A5: (W .weightSeq()) . n in rng (the_Weight_of G) by A4, FUNCT_1:def 3;
rng (the_Weight_of G) c= Real>=0 by Def14;
then (W .weightSeq()) . n in Real>=0 by A5;
then ex r being Real st
( r = (W .weightSeq()) . n & r >= 0 ) by GRAPH_5:def 12;
hence 0 <= (W .weightSeq()) . n ; :: thesis: verum