let G be _Graph; :: thesis:
let W1, W2 be Walk of G; :: thesis:
let n be Element of NAT ; :: thesis:
set W3 = W1 .append W2;
assume A1: n in dom (W1 .append W2) ; :: thesis:
then A2: n <= len (W1 .append W2) by FINSEQ_3:25;
A3: 1 <= n by A1, FINSEQ_3:25;

now :: thesis:

per cases ;

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

then A4: (len (W1 .append W2)) + 1 = (len W1) + (len W2) by Lm9;

now :: thesis:

assume not n in dom W1 ; :: thesis:
then len W1 < n by A3, FINSEQ_3:25;
then reconsider k = n - (len W1) as Element of NAT by INT_1:5;
take k = k; :: thesis:

now :: thesis:

assume len W2 <= k ; :: thesis:
then (len W1) + (len W2) <= (len W1) + k by XREAL_1:7;
hence contradiction by A2, A4, NAT_1:13; :: thesis:

end;

hence k < len W2 ; :: thesis:
thus n = (len W1) + k ; :: thesis:

end;

hence ( n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) ) ; :: thesis:

end;

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

hence ( n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) ) by A1, Def10; :: thesis:

end;

end;

end;

hence ( n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) ) ; :: thesis: