let G be _Graph; :: thesis: for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
for n being Element of NAT st n < len W2 holds
( (W1 .append W2) . ((len W1) + n) = W2 . (n + 1) & (len W1) + n in dom (W1 .append W2) )
let W1, W2 be Walk of G; :: thesis: ( W1 .last() = W2 .first() implies for n being Element of NAT st n < len W2 holds
( (W1 .append W2) . ((len W1) + n) = W2 . (n + 1) & (len W1) + n in dom (W1 .append W2) ) )
set W = W1 .append W2;
assume A1: W1 .last() = W2 .first() ; :: thesis: for n being Element of NAT st n < len W2 holds
( (W1 .append W2) . ((len W1) + n) = W2 . (n + 1) & (len W1) + n in dom (W1 .append W2) )
let n be Element of NAT ; :: thesis: ( n < len W2 implies ( (W1 .append W2) . ((len W1) + n) = W2 . (n + 1) & (len W1) + n in dom (W1 .append W2) ) )
assume A2: n < len W2 ; :: thesis: ( (W1 .append W2) . ((len W1) + n) = W2 . (n + 1) & (len W1) + n in dom (W1 .append W2) )
then n + 1 <= len W2 by NAT_1:13;
then (n + 1) + (len W1) <= (len W2) + (len W1) by XREAL_1:7;
then ((len W1) + n) + 1 <= (len (W1 .append W2)) + 1 by A1, Lm9;
then A3: (len W1) + n <= len (W1 .append W2) by XREAL_1:6;
A4: W1 .append W2 = W1 ^' W2 by A1, Def10;

now :: thesis: (W1 .append W2) . ((len W1) + n) = W2 . (n + 1)

per cases ( n = 0 or n <> 0 ) ;

suppose A5: n = 0 ; :: thesis: (W1 .append W2) . ((len W1) + n) = W2 . (n + 1)

then 1 <= (len W1) + n by ABIAN:12;
then (len W1) + n in dom W1 by A5, FINSEQ_3:25;
hence (W1 .append W2) . ((len W1) + n) = W2 . (n + 1) by A1, A5, Lm12; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: (W1 .append W2) . ((len W1) + n) = W2 . (n + 1)

then 0 + 1 < n + 1 by XREAL_1:8;
then 1 <= n by NAT_1:13;
hence (W1 .append W2) . ((len W1) + n) = W2 . (n + 1) by A4, A2, FINSEQ_6:141; :: thesis: verum

end;

end;

end;

hence (W1 .append W2) . ((len W1) + n) = W2 . (n + 1) ; :: thesis: (len W1) + n in dom (W1 .append W2)
1 <= (len W1) + n by ABIAN:12, NAT_1:12;
hence (len W1) + n in dom (W1 .append W2) by A3, FINSEQ_3:25; :: thesis: verum