theorem Th4: :: GRAPHSP:4

for G being Graph
for pe being FinSequence of the carrier' of G
for W being Function st W is_weight_of G & len pe = 1 holds
cost (pe,W) = W . (pe . 1)