let W be Function; :: thesis: for G being Graph
for pe being FinSequence of the carrier' of G
for p being oriented Chain of G st pe in AcyclicPaths p & W is_weight>=0of G holds
cost (pe,W) <= cost (p,W)
let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G
for p being oriented Chain of G st pe in AcyclicPaths p & W is_weight>=0of G holds
cost (pe,W) <= cost (p,W)
let pe be FinSequence of the carrier' of G; :: thesis: for p being oriented Chain of G st pe in AcyclicPaths p & W is_weight>=0of G holds
cost (pe,W) <= cost (p,W)
let p be oriented Chain of G; :: thesis: ( pe in AcyclicPaths p & W is_weight>=0of G implies cost (pe,W) <= cost (p,W) )
assume that
A1: pe in AcyclicPaths p and
A2: W is_weight>=0of G ; :: thesis: cost (pe,W) <= cost (p,W)
A3: ex r being oriented Simple Chain of G st
( r = pe & r <> {} & the Source of G . (r . 1) = the Source of G . (p . 1) & the Target of G . (r . (len r)) = the Target of G . (p . (len p)) & rng r c= rng p ) by A1;
then pe is one-to-one by Th20;
hence cost (pe,W) <= cost (p,W) by A2, A3, Th59; :: thesis: verum