let G be real-weighted WGraph; :: thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .cost() = (W1 .cost()) + (W2 .cost())
let W1, W2 be Walk of G; :: thesis: ( W1 .last() = W2 .first() implies (W1 .append W2) .cost() = (W1 .cost()) + (W2 .cost()) )
set W3 = W1 .append W2;
assume W1 .last() = W2 .first() ; :: thesis: (W1 .append W2) .cost() = (W1 .cost()) + (W2 .cost())
then (W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq()) by Th16;
hence (W1 .append W2) .cost() = (W1 .cost()) + (W2 .cost()) by RVSUM_1:75; :: thesis: verum