let W be Function; :: thesis: for G being Graph
for pe being FinSequence of the carrier' of G st W is_weight>=0of G holds
cost (pe,W) >= 0
let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G st W is_weight>=0of G holds
cost (pe,W) >= 0
let pe be FinSequence of the carrier' of G; :: thesis: ( W is_weight>=0of G implies cost (pe,W) >= 0 )
set f = RealSequence (pe,W);
assume W is_weight>=0of G ; :: thesis: cost (pe,W) >= 0
then for i being Nat st i in dom (RealSequence (pe,W)) holds
(RealSequence (pe,W)) . i >= 0 by Th45;
hence cost (pe,W) >= 0 by RVSUM_1:84; :: thesis: verum