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 Th23;
hence (W1 .append W2) .cost() = (W1 .cost() ) + (W2 .cost() ) by RVSUM_1:105; :: thesis: verum