for W being Function
for G being Graph
for pe, qe being FinSequence of the carrier' of G st qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G holds
cost (qe,W) <= cost (pe,W)