let G be nonnegative-weighted WGraph; :: thesis: for W1 being Walk of G
for W2 being Subwalk of W1 holds W2 .cost() <= W1 .cost()
let W1 be Walk of G; :: thesis: for W2 being Subwalk of W1 holds W2 .cost() <= W1 .cost()
let W2 be Subwalk of W1; :: thesis: W2 .cost() <= W1 .cost()
consider ws being Subset of (W1 .weightSeq() ) such that
A1: W2 .weightSeq() = Seq ws by Th25;
for i being Element of NAT st i in dom (W1 .weightSeq() ) holds
0 <= (W1 .weightSeq() ) . i by Th35;
hence W2 .cost() <= W1 .cost() by A1, Th2; :: thesis: verum