let G be _Graph; :: thesis: for W1, W2 being Walk of G st W2 is V5() holds
W1 .append W2 = W1
let W1, W2 be Walk of G; :: thesis: ( W2 is V5() implies W1 .append W2 = W1 )
assume W2 is V5() ; :: thesis: W1 .append W2 = W1
then A1: len W2 = 1 by Lm55;
now :: thesis: W1 .append W2 = W1
per cases ( W1 .last() = W2 .first() or W1 .last() <> W2 .first() ) ;
suppose W1 .last() = W2 .first() ; :: thesis: W1 .append W2 = W1
then A2: W1 .append W2 = W1 ^' W2 by Def10;
then A3: (len (W1 .append W2)) + 1 = (len W1) + 1 by A1, CARD_1:27, FINSEQ_6:139;
for k being Nat st 1 <= k & k <= len (W1 .append W2) holds
(W1 .append W2) . k = W1 . k by A2, A3, FINSEQ_6:140;
hence W1 .append W2 = W1 by A3, FINSEQ_1:14; :: thesis: verum
end;
end;
end;
hence W1 .append W2 = W1 ; :: thesis: verum