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:29
.= 0 by A1 ;
then RealSequence (pe,W) = <*> REAL ;
hence cost (pe,W) = 0 by RVSUM_1:72; :: thesis: verum