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