:: deftheorem Def15 defines RealSequence GRAPH_5:def 15 :
for G being Graph
for p being FinSequence of the carrier' of G
for W being Function st W is_weight_of G holds
for b₄ being FinSequence of REAL holds
( b₄ = RealSequence (p,W) iff ( dom p = dom b₄ & ( for i being Nat st i in dom p holds
b₄ . i = W . (p . i) ) ) );