let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G
for W being Function st W is_weight_of G & len pe = 1 holds
cost (pe,W) = W . (pe . 1)
let pe be FinSequence of the carrier' of G; :: thesis: for W being Function st W is_weight_of G & len pe = 1 holds
cost (pe,W) = W . (pe . 1)
let W be Function; :: thesis: ( W is_weight_of G & len pe = 1 implies cost (pe,W) = W . (pe . 1) )
assume that
A1: W is_weight_of G and
A2: len pe = 1 ; :: thesis: cost (pe,W) = W . (pe . 1)
A3: 1 in dom pe by A2, FINSEQ_3:27;
set f = RealSequence (pe,W);
dom (RealSequence (pe,W)) = dom pe by A1, GRAPH_5:def 15;
then len (RealSequence (pe,W)) = 1 by A2, FINSEQ_3:31;
then A4: RealSequence (pe,W) = <*((RealSequence (pe,W)) . 1)*> by FINSEQ_1:57;
thus cost (pe,W) = Sum (RealSequence (pe,W)) by GRAPH_5:def 16
.= (RealSequence (pe,W)) . 1 by A4, FINSOP_1:12
.= W . (pe . 1) by A1, A3, GRAPH_5:def 15 ; :: thesis: verum