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:25;
set f = RealSequence (pe,W);
reconsider f1 = (RealSequence (pe,W)) . 1 as Element of REAL by XREAL_0:def 1;
dom (RealSequence (pe,W)) = dom pe by A1, GRAPH_5:def 15;
then len (RealSequence (pe,W)) = 1 by A2, FINSEQ_3:29;
then A4: RealSequence (pe,W) = <*f1*> by FINSEQ_1:40;
thus cost (pe,W) = Sum (RealSequence (pe,W)) by GRAPH_5:def 16
.= (RealSequence (pe,W)) . 1 by A4, FINSOP_1:11
.= W . (pe . 1) by A1, A3, GRAPH_5:def 15 ; :: thesis: verum