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

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