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 n in dom (W .weightSeq() ) ; :: thesis: 0 <= (W .weightSeq() ) . n
then A1: ( 1 <= n & n <= len (W .weightSeq() ) ) by FINSEQ_3:27;
then A2: (W .weightSeq() ) . n = (the_Weight_of G) . ((W .edgeSeq() ) . n) by Def18;
A3: dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def 4;
( 1 <= n & n <= len (W .edgeSeq() ) ) by A1, Def18;
then n in dom (W .edgeSeq() ) by FINSEQ_3:27;
then (W .edgeSeq() ) . n in dom (the_Weight_of G) by A3, GLIB_001:80;
then A4: (W .weightSeq() ) . n in rng (the_Weight_of G) by A2, FUNCT_1:def 5;
rng (the_Weight_of G) c= Real>=0 by Def14;
then (W .weightSeq() ) . n in Real>=0 by A4;
then consider r being Real such that
A5: ( r = (W .weightSeq() ) . n & r >= 0 ) by GRAPH_5:def 12;
thus 0 <= (W .weightSeq() ) . n by A5; :: thesis: verum