let G be _Graph; :: thesis: for W1, W2 being Walk of G

for n being Element of NAT st n in dom W1 holds

( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) )

let W1, W2 be Walk of G; :: thesis: for n being Element of NAT st n in dom W1 holds

( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) )

let n be Element of NAT ; :: thesis: ( n in dom W1 implies ( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) ) )

set W = W1 .append W2;

assume A1: n in dom W1 ; :: thesis: ( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) )

then A2: n <= len W1 by FINSEQ_3:25;

A3: 1 <= n by A1, FINSEQ_3:25;

for n being Element of NAT st n in dom W1 holds

( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) )

let W1, W2 be Walk of G; :: thesis: for n being Element of NAT st n in dom W1 holds

( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) )

let n be Element of NAT ; :: thesis: ( n in dom W1 implies ( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) ) )

set W = W1 .append W2;

assume A1: n in dom W1 ; :: thesis: ( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) )

then A2: n <= len W1 by FINSEQ_3:25;

A3: 1 <= n by A1, FINSEQ_3:25;

now :: thesis: ( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) )end;

hence
( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) )
; :: thesis: verumper cases
( W1 .last() = W2 .first() or W1 .last() <> W2 .first() )
;

end;

suppose A4:
W1 .last() = W2 .first()
; :: thesis: ( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) )

then
W1 .append W2 = W1 ^' W2
by Def10;

hence (W1 .append W2) . n = W1 . n by A3, A2, FINSEQ_6:140; :: thesis: n in dom (W1 .append W2)

reconsider lenW2aa1 = (len W2) - 1 as Element of NAT by ABIAN:12, INT_1:5;

n <= (len W1) + lenW2aa1 by A2, NAT_1:12;

then n <= ((len W1) + (len W2)) + (- 1) ;

then n <= ((len (W1 .append W2)) + 1) + (- 1) by A4, Lm9;

hence n in dom (W1 .append W2) by A3, FINSEQ_3:25; :: thesis: verum

end;hence (W1 .append W2) . n = W1 . n by A3, A2, FINSEQ_6:140; :: thesis: n in dom (W1 .append W2)

reconsider lenW2aa1 = (len W2) - 1 as Element of NAT by ABIAN:12, INT_1:5;

n <= (len W1) + lenW2aa1 by A2, NAT_1:12;

then n <= ((len W1) + (len W2)) + (- 1) ;

then n <= ((len (W1 .append W2)) + 1) + (- 1) by A4, Lm9;

hence n in dom (W1 .append W2) by A3, FINSEQ_3:25; :: thesis: verum