let W be Function; :: thesis: for G being Graph
for pe, qe being FinSequence of the carrier' of G st qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G holds
cost (qe,W) <= cost (pe,W)
let G be Graph; :: thesis: for pe, qe being FinSequence of the carrier' of G st qe is one-to-one & 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; :: thesis: ( qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G implies cost (qe,W) <= cost (pe,W) )
set D = the carrier' of G;
assume that
A1: ( qe is one-to-one & rng qe c= rng pe ) and
A2: W is_weight>=0of G ; :: thesis: cost (qe,W) <= cost (pe,W)
defpred S₁[ Nat] means for p, q being FinSequence of the carrier' of G st q is one-to-one & rng q c= rng p & len q = $1 holds
cost (q,W) <= cost (p,W);
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for p, q being FinSequence of the carrier' of G st q is one-to-one & rng q c= rng p & len q = k + 1 holds
cost (q,W) <= cost (p,W)

let p, q be FinSequence of the carrier' of G; :: thesis: ( q is one-to-one & rng q c= rng p & len q = k + 1 implies cost (q,W) <= cost (p,W) )
assume that
A5: q is one-to-one and
A6: rng q c= rng p and
A7: len q = k + 1 ; :: thesis: cost (q,W) <= cost (p,W)
consider q1 being FinSequence, x being object such that
A8: q = q1 ^ <*x*> by A7, FINSEQ_2:18;
A9: k + 1 = (len q1) + 1 by A7, A8, FINSEQ_2:16;
consider p1, p2 being FinSequence such that
A10: p = (p1 ^ <*x*>) ^ p2 and
A11: rng q1 c= rng (p1 ^ p2) by A5, A6, A8, Th7;
reconsider q1 = q1 as FinSequence of the carrier' of G by A8, FINSEQ_1:36;
A12: p1 ^ <*x*> is FinSequence of the carrier' of G by A10, FINSEQ_1:36;
then reconsider y = <*x*> as FinSequence of the carrier' of G by FINSEQ_1:36;
reconsider p2 = p2 as FinSequence of the carrier' of G by A10, FINSEQ_1:36;
reconsider p1 = p1 as FinSequence of the carrier' of G by A12, FINSEQ_1:36;
q1 is one-to-one by A5, A8, FINSEQ_3:91;
then A13: cost (q1,W) <= cost ((p1 ^ p2),W) by A4, A11, A9;
A14: cost (q,W) = (cost (q1,W)) + (cost (y,W)) by A2, A8, Th44, Th52;
cost (p,W) = (cost ((p1 ^ y),W)) + (cost (p2,W)) by A2, A10, Th44, Th52
.= ((cost (p1,W)) + (cost (y,W))) + (cost (p2,W)) by A2, Th44, Th52
.= ((cost (p1,W)) + (cost (p2,W))) + (cost (y,W))
.= (cost ((p1 ^ p2),W)) + (cost (y,W)) by A2, Th44, Th52 ;
hence cost (q,W) <= cost (p,W) by A14, A13, XREAL_1:7; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A15: S₁[ 0 ]

proof

let p, q be FinSequence of the carrier' of G; :: thesis: ( q is one-to-one & rng q c= rng p & len q = 0 implies cost (q,W) <= cost (p,W) )
assume that
q is one-to-one and
rng q c= rng p and
A16: len q = 0 ; :: thesis: cost (q,W) <= cost (p,W)
q = {} by A16;
then cost (q,W) = 0 by A2, Th44, Th49;
hence cost (q,W) <= cost (p,W) by A2, Th48; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A15, A3);
then S₁[ len qe] ;
hence cost (qe,W) <= cost (pe,W) by A1; :: thesis: verum