theorem Th45: :: GRAPH_5:47

for W being Function
for G being Graph
for pe being FinSequence of the carrier' of G
for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence (pe,W) holds
for i being Nat st i in dom f holds
f . i >= 0