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;

( k < len W2 & n = (len W1) + k ) ) ; :: thesis: verum

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 :: thesis: ( n in dom W1 or ex k being Element of NAT st

( k < len W2 & n = (len W1) + k ) )end;

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

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

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 ) )

( k < len W2 & n = (len W1) + k ) )

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

( k < len W2 & n = (len W1) + k ) ) ; :: thesis: verum

end;now :: thesis: ( not n in dom W1 implies 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 ) )

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 )

thus n = (len W1) + k ; :: thesis: verum

end;( 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 :: thesis: not len W2 <= k

hence
k < len W2
; :: thesis: n = (len W1) + kassume
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;then (len W1) + (len W2) <= (len W1) + k by XREAL_1:7;

hence contradiction by A2, A4, NAT_1:13; :: thesis: verum

thus n = (len W1) + k ; :: thesis: verum

( k < len W2 & n = (len W1) + k ) ) ; :: thesis: verum

( k < len W2 & n = (len W1) + k ) ) ; :: thesis: verum