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 A1, FINSEQ_3:25;

now

per cases ( W1 .last() = W2 .first() or W1 .last() <> W2 .first() ) ;

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

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 A3, FINSEQ_3:25;
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

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 A1, Def10; :: 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