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 A1: ( W is_weight_of G & len pe = 1 ) ; :: thesis: cost pe,W = W . (pe . 1)
set f = RealSequence pe,W;
A2: ( dom (RealSequence pe,W) = dom pe & ( for i being Element of NAT st i in dom pe holds
(RealSequence pe,W) . i = W . (pe . i) ) ) by A1, GRAPH_5:def 15;
A3: 1 in dom pe by A1, FINSEQ_3:27;
len (RealSequence pe,W) = 1 by A1, 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