let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 is trivial & W1 .last() = W2 .first() holds
W1 .append W2 = W2
let W1, W2 be Walk of G; :: thesis: ( W1 is trivial & W1 .last() = W2 .first() implies W1 .append W2 = W2 )
assume that
A1: W1 is trivial and
A2: W1 .last() = W2 .first() ; :: thesis: W1 .append W2 = W2
A3: len W1 = 1 by A1, GLIB_001:126;
then A4: (len (W1 .append W2)) + 1 = 1 + (len W2) by A2, GLIB_001:28;

now :: thesis: for k being Nat st 1 <= k & k <= len (W1 .append W2) holds
(W1 .append W2) . k = W2 . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (W1 .append W2) implies (W1 .append W2) . k = W2 . k )
assume that
A5: 1 <= k and
A6: k <= len (W1 .append W2) ; :: thesis: (W1 .append W2) . k = W2 . k
1 - 1 <= k - 1 by A5, XREAL_1:9;
then reconsider k1 = k - 1 as Element of NAT by INT_1:3;
k - 1 < k by XREAL_1:44;
then k - 1 < len W2 by A4, A6, XXREAL_0:2;
then (W1 .append W2) . (1 + k1) = W2 . (k1 + 1) by A2, A3, GLIB_001:33;
hence (W1 .append W2) . k = W2 . k ; :: thesis: verum

end;

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