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 A1: ( W1 is trivial & W1 .last() = W2 .first() ) ; :: thesis: W1 .append W2 = W2
A2: len W1 = 1 by A1, GLIB_001:127;
then A3: (len (W1 .append W2)) + 1 = 1 + (len W2) by A1, GLIB_001:29;

now

let k be Nat; :: thesis: ( 1 <= k & k <= len (W1 .append W2) implies (W1 .append W2) . k = W2 . k )
assume A4: ( 1 <= k & k <= len (W1 .append W2) ) ; :: thesis: (W1 .append W2) . k = W2 . k
A5: 1 - 1 <= k - 1 by A4, XREAL_1:11;
k - 1 < k by XREAL_1:46;
then A6: ( 0 <= k - 1 & k - 1 < len W2 ) by A3, A4, A5, XXREAL_0:2;
reconsider k1 = k - 1 as Element of NAT by A5, INT_1:16;
(W1 .append W2) . (1 + k1) = W2 . (k1 + 1) by A1, A2, A6, GLIB_001:34;
hence (W1 .append W2) . k = W2 . k ; :: thesis: verum

end;

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