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 Th51;
hence cost pe,W >= 0 by RVSUM_1:114; :: thesis: verum