let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .length() = (W1 .length()) + (W2 .length())
let P, H be Walk of G; :: thesis: ( P .last() = H .first() implies (P .append H) .length() = (P .length()) + (H .length()) )
assume H .first() = P .last() ; :: thesis: (P .append H) .length() = (P .length()) + (H .length())
hence (P .append H) .length() = len ((P .edgeSeq()) ^ (H .edgeSeq())) by GLIB_001:85
.= (P .length()) + (H .length()) by FINSEQ_1:22 ;
:: thesis: verum