let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(len (W1 .append W2)) + 1 = (len W1) + (len W2)
let W1, W2 be Walk of G; :: thesis: ( W1 .last() = W2 .first() implies (len (W1 .append W2)) + 1 = (len W1) + (len W2) )
set W = W1 .append W2;
assume W1 .last() = W2 .first() ; :: thesis: (len (W1 .append W2)) + 1 = (len W1) + (len W2)
then W1 .append W2 = W1 ^' W2 by Def10;
hence (len (W1 .append W2)) + 1 = (len W1) + (len W2) by CARD_1:27, FINSEQ_6:139; :: thesis: verum