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;

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

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

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;

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

hence ( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) ) by A1, Def10; :: thesis: verum

end;

end;

end;

hence ( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) ) ; :: thesis: verum