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 ;
then A3: (len W1) + n <= len (W1 .append W2) by XREAL_1:6;
A4: W1 .append W2 = W1 ^' W2 by ;
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 ;
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 ; :: 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 ;
hence (len W1) + n in dom (W1 .append W2) by ; :: thesis: verum