let G be _Graph; :: thesis: for W2, W1 being Walk of G st W2 is trivial holds
W1 .append W2 = W1
let W2, W1 be Walk of G; :: thesis: ( W2 is trivial implies W1 .append W2 = W1 )
assume W2 is trivial ; :: thesis: W1 .append W2 = W1
then A1: len W2 = 1 by Lm55;

now

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, GRAPH_2:13;
for k being Nat st 1 <= k & k <= len (W1 .append W2) holds
(W1 .append W2) . k = W1 . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (W1 .append W2) implies (W1 .append W2) . k = W1 . k )
reconsider k = k as Element of NAT by ORDINAL1:def 12;
( 1 <= k & k <= len (W1 .append W2) implies (W1 .append W2) . k = W1 . k ) by A2, A3, GRAPH_2:14;
hence ( 1 <= k & k <= len (W1 .append W2) implies (W1 .append W2) . k = W1 . k ) ; :: thesis: verum

end;

hence W1 .append W2 = W1 by A3, FINSEQ_1:14; :: thesis: verum

end;

suppose W1 .last() <> W2 .first() ; :: thesis: W1 .append W2 = W1

hence W1 .append W2 = W1 by Def10; :: thesis: verum

end;

end;

end;

hence W1 .append W2 = W1 ; :: thesis: verum