let W be Function; 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; 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; ( pe = {} & W is_weight_of G implies cost (pe,W) = 0 )
assume that
A1:
pe = {}
and
A2:
W is_weight_of G
; 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; verum