let W be Function; :: thesis: for G being Graph
for qe, pe being FinSequence of the carrier' of G st len qe = 1 & rng qe c= rng pe & W is_weight>=0of G holds
cost qe,W <= cost pe,W
let G be Graph; :: thesis: for qe, pe being FinSequence of the carrier' of G st len qe = 1 & rng qe c= rng pe & W is_weight>=0of G holds
cost qe,W <= cost pe,W
let qe, pe be FinSequence of the carrier' of G; :: thesis: ( len qe = 1 & rng qe c= rng pe & W is_weight>=0of G implies cost qe,W <= cost pe,W )
assume that
A1: len qe = 1 and
A2: rng qe c= rng pe and
A3: W is_weight>=0of G ; :: thesis: cost qe,W <= cost pe,W
set f = RealSequence pe,W;
set g = RealSequence qe,W;
1 in dom qe by A1, FINSEQ_3:27;
then consider j being Element of NAT such that
A4: j in dom pe and
A5: (RealSequence pe,W) . j = (RealSequence qe,W) . 1 by A2, A3, Th50, Th52;
A6: W is_weight_of G by A3, Th50;
then dom pe = dom (RealSequence pe,W) by Def15;
then A7: len pe = len (RealSequence pe,W) by FINSEQ_3:31;
dom (RealSequence qe,W) = dom qe by A6, Def15;
then len (RealSequence qe,W) = len qe by FINSEQ_3:31;
then RealSequence qe,W = <*((RealSequence qe,W) . 1)*> by A1, FINSEQ_1:57;
then A8: cost qe,W = (RealSequence qe,W) . 1 by FINSOP_1:12;
j <= len pe by A4, FINSEQ_3:27;
then consider m being Nat such that
A9: len (RealSequence pe,W) = j + m by A7, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
consider f1, f2 being FinSequence of REAL such that
A10: len f1 = j and
len f2 = m and
A11: RealSequence pe,W = f1 ^ f2 by A9, FINSEQ_2:26;
A12: 1 <= j by A4, FINSEQ_3:27;
then consider h being FinSequence of REAL , d being Real such that
A13: f1 = h ^ <*d*> by A10, FINSEQ_2:22;
j in dom f1 by A12, A10, FINSEQ_3:27;
then A14: f1 . j = (RealSequence qe,W) . 1 by A5, A11, FINSEQ_1:def 7;
j = (len h) + 1 by A10, A13, FINSEQ_2:19;
then A15: d = (RealSequence qe,W) . 1 by A13, A14, FINSEQ_1:59;
for i being Nat st i in dom (RealSequence pe,W) holds
(RealSequence pe,W) . i >= 0 by A3, Th51;
then A16: for y being Real st y in rng (RealSequence pe,W) holds
y >= 0 by Lm3;
then for i being Nat st i in dom f2 holds
f2 . i >= 0 by A11, Lm4;
then A17: Sum f2 >= 0 by RVSUM_1:114;
for i being Nat st i in dom f1 holds
f1 . i >= 0 by A11, A16, Lm4;
then for y being Real st y in rng f1 holds
y >= 0 by Lm3;
then for i being Nat st i in dom h holds
h . i >= 0 by A13, Lm4;
then A18: Sum h >= 0 by RVSUM_1:114;
Sum f1 = (Sum h) + (Sum <*d*>) by A13, RVSUM_1:105
.= (Sum h) + ((RealSequence qe,W) . 1) by A15, FINSOP_1:12 ;
then A19: Sum f1 >= 0 + ((RealSequence qe,W) . 1) by A18, XREAL_1:9;
Sum (RealSequence pe,W) = (Sum f1) + (Sum f2) by A11, RVSUM_1:105;
hence cost qe,W <= cost pe,W by A8, A17, A19, XREAL_1:9; :: thesis: verum