let W be Function; :: thesis: for G being Graph
for pe being FinSequence of the carrier' of G st pe = {} & W is_weight_of G holds
cost pe,W = 0
let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G st pe = {} & W is_weight_of G holds
cost pe,W = 0
let pe be FinSequence of the carrier' of G; :: thesis: ( pe = {} & W is_weight_of G implies cost pe,W = 0 )
assume that
A1: pe = {} and
A2: W is_weight_of G ; :: thesis: cost pe,W = 0
set f = RealSequence pe,W;
dom (RealSequence pe,W) = dom pe by A2, Def15;
then len (RealSequence pe,W) = len pe by FINSEQ_3:31
.= 0 by A1 ;
then RealSequence pe,W = <*> REAL ;
hence cost pe,W = 0 by RVSUM_1:102; :: thesis: verum