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 ) ;

suppose A4: len W2 <> 1 ; :: thesis: (W1 .append W2) .last() = W2 .last()

1 <= len W2 by ABIAN:12;
then 1 < len W2 by A4, XXREAL_0:1;
hence (W1 .append W2) .last() = W2 .last() by A2, FINSEQ_6:142; :: thesis: verum

end;

suppose A5: len W2 = 1 ; :: thesis: (W1 .append W2) .last() = W2 .last()

A6: (2,1) -cut W2 = {} by FINSEQ_6:def 4;
W1 .append W2 = W1 ^ ((2,1) -cut W2) by A2, A5, FINSEQ_6:def 5;
hence (W1 .append W2) .last() = W2 .last() by A1, A5, A6, FINSEQ_1:34; :: thesis: verum

end;

end;

end;

hence ( (W1 .append W2) .last() = W2 .last() & W1 .append W2 is_Walk_from W1 .first() ,W2 .last() ) by A3; :: thesis: verum