let G be _Graph; :: thesis: for W1, W2 being Walk of G
for n being Element of NAT holds
( not n in dom (W1 .append W2) or n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) )

let W1, W2 be Walk of G; :: thesis: for n being Element of NAT holds
( not n in dom (W1 .append W2) or n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) )

let n be Element of NAT ; :: thesis: ( not n in dom (W1 .append W2) or n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) )

set W3 = W1 .append W2;
assume A1: n in dom (W1 .append W2) ; :: thesis: ( n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) )

then A2: n <= len (W1 .append W2) by FINSEQ_3:25;
A3: 1 <= n by ;
now :: thesis: ( n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) )
per cases ;
suppose W1 .last() = W2 .first() ; :: thesis: ( n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) )

then A4: (len (W1 .append W2)) + 1 = (len W1) + (len W2) by Lm9;
now :: thesis: ( not n in dom W1 implies ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) )
assume not n in dom W1 ; :: thesis: ex k being Element of NAT st
( k < len W2 & n = (len W1) + k )

then len W1 < n by ;
then reconsider k = n - (len W1) as Element of NAT by INT_1:5;
take k = k; :: thesis: ( k < len W2 & n = (len W1) + k )
now :: thesis: not len W2 <= k
assume len W2 <= k ; :: thesis: contradiction
then (len W1) + (len W2) <= (len W1) + k by XREAL_1:7;
hence contradiction by A2, A4, NAT_1:13; :: thesis: verum
end;
hence k < len W2 ; :: thesis: n = (len W1) + k
thus n = (len W1) + k ; :: thesis: verum
end;
hence ( n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) ) ; :: thesis: verum
end;
suppose W1 .last() <> W2 .first() ; :: thesis: ( n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) )

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