let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
( (W1 .append W2) .first() = W1 .first() & (W1 .append W2) .last() = W2 .last() & W1 .append W2 is_Walk_from W1 .first() ,W2 .last() )
let W1, W2 be Walk of G; :: thesis: ( W1 .last() = W2 .first() implies ( (W1 .append W2) .first() = W1 .first() & (W1 .append W2) .last() = W2 .last() & W1 .append W2 is_Walk_from W1 .first() ,W2 .last() ) )
set W = W1 .append W2;
assume A1: W1 .last() = W2 .first() ; :: thesis: ( (W1 .append W2) .first() = W1 .first() & (W1 .append W2) .last() = W2 .last() & W1 .append W2 is_Walk_from W1 .first() ,W2 .last() )
then A2: W1 .append W2 = W1 ^' W2 by Def10;
1 <= len W1 by ABIAN:12;
hence A3: (W1 .append W2) .first() = W1 .first() by A2, FINSEQ_6:140; :: thesis: ( (W1 .append W2) .last() = W2 .last() & W1 .append W2 is_Walk_from W1 .first() ,W2 .last() )
now :: thesis: (W1 .append W2) .last() = W2 .last()
per cases ( len W2 <> 1 or len W2 = 1 ) ;
end;
end;
hence ( (W1 .append W2) .last() = W2 .last() & W1 .append W2 is_Walk_from W1 .first() ,W2 .last() ) by A3; :: thesis: verum