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:27;
A3: n <= len (W .weightSeq() ) by A1, FINSEQ_3:27;
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:27, PARTFUN1:def 4;
then A4: (W .edgeSeq() ) . n in dom (the_Weight_of G) by GLIB_001:80;
(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 5;
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