let W be Function; for G being Graph
for pe, qe 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; for pe, qe 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 pe, qe be FinSequence of the carrier' of G; ( 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
; cost (qe,W) <= cost (pe,W)
set f = RealSequence (pe,W);
set g = RealSequence (qe,W);
1 in dom qe
by A1, FINSEQ_3:25;
then consider j being Nat such that
A4:
j in dom pe
and
A5:
(RealSequence (pe,W)) . j = (RealSequence (qe,W)) . 1
by A2, A3, Th44, Th46;
A6:
W is_weight_of G
by A3, Th44;
then
dom pe = dom (RealSequence (pe,W))
by Def15;
then A7:
len pe = len (RealSequence (pe,W))
by FINSEQ_3:29;
reconsider g1 = (RealSequence (qe,W)) . 1 as Element of REAL by XREAL_0:def 1;
dom (RealSequence (qe,W)) = dom qe
by A6, Def15;
then
len (RealSequence (qe,W)) = len qe
by FINSEQ_3:29;
then
RealSequence (qe,W) = <*g1*>
by A1, FINSEQ_1:40;
then
Sum (RealSequence (qe,W)) = g1
by RVSUM_1:73;
then A8:
cost (qe,W) = g1
;
j <= len pe
by A4, FINSEQ_3:25;
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 12;
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:23;
A12:
1 <= j
by A4, FINSEQ_3:25;
then consider h being FinSequence of REAL , d being Element of REAL such that
A13:
f1 = h ^ <*d*>
by A10, FINSEQ_2:19;
j in dom f1
by A12, A10, FINSEQ_3:25;
then A14:
f1 . j = (RealSequence (qe,W)) . 1
by A5, A11, FINSEQ_1:def 7;
j = (len h) + 1
by A10, A13, FINSEQ_2:16;
then A15:
d = (RealSequence (qe,W)) . 1
by A13, A14, FINSEQ_1:42;
for i being Nat st i in dom (RealSequence (pe,W)) holds
(RealSequence (pe,W)) . i >= 0
by A3, Th45;
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:84;
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:84;
reconsider d = d as Element of REAL ;
reconsider dd = <*d*> as FinSequence of REAL ;
Sum f1 =
(Sum h) + (Sum dd)
by A13, RVSUM_1:75
.=
(Sum h) + d
by RVSUM_1:73
.=
(Sum h) + ((RealSequence (qe,W)) . 1)
by A15
;
then A19:
Sum f1 >= 0 + ((RealSequence (qe,W)) . 1)
by A18, XREAL_1:7;
Sum (RealSequence (pe,W)) = (Sum f1) + (Sum f2)
by A11, RVSUM_1:75;
hence
cost (qe,W) <= cost (pe,W)
by A8, A17, A19, XREAL_1:7; verum