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 ;
now :: thesis: ( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) )
per cases ;
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 ; :: thesis: n in dom (W1 .append W2)
reconsider lenW2aa1 = (len W2) - 1 as Element of NAT by ;
n <= (len W1) + lenW2aa1 by ;
then n <= ((len W1) + (len W2)) + (- 1) ;
then n <= ((len (W1 .append W2)) + 1) + (- 1) by ;
hence n in dom (W1 .append W2) by ; :: 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 ; :: thesis: verum
end;
end;
end;
hence ( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) ) ; :: thesis: verum