let G be _Graph; :: thesis: for W being Walk of G
for m, n, o being odd Element of NAT st m <= n & n <= o & o <= len W holds
(W .cut m,n) .append (W .cut n,o) = W .cut m,o
let W be Walk of G; :: thesis: for m, n, o being odd Element of NAT st m <= n & n <= o & o <= len W holds
(W .cut m,n) .append (W .cut n,o) = W .cut m,o
let m, n, o be odd Element of NAT ; :: thesis: ( m <= n & n <= o & o <= len W implies (W .cut m,n) .append (W .cut n,o) = W .cut m,o )
assume A1: ( m <= n & n <= o & o <= len W ) ; :: thesis: (W .cut m,n) .append (W .cut n,o) = W .cut m,o
then A2: ( m <= o & n <= len W ) by XXREAL_0:2;
set W1 = W .cut m,n;
set W2 = W .cut n,o;
set W3 = W .cut m,o;
set W4 = (W .cut m,n) .append (W .cut n,o);

now

A3: (W .cut m,n) .last() = W . n by A1, A2, Lm16
.= (W .cut n,o) .first() by A1, Lm16 ;
A4: (len (W .cut m,n)) + m = n + 1 by A1, A2, Lm15;
A5: (len (W .cut n,o)) + n = o + 1 by A1, Lm15;
A6: (len (W .cut m,o)) + m = o + 1 by A1, A2, Lm15;
then ((len (W .cut m,n)) + (len (W .cut n,o))) + m = (1 + (len (W .cut m,o))) + m by A4, A5;
then A7: (len ((W .cut m,n) .append (W .cut n,o))) + 1 = (len (W .cut m,o)) + 1 by A3, Lm9;
hence ( len ((W .cut m,n) .append (W .cut n,o)) = len ((W .cut m,n) .append (W .cut n,o)) & len (W .cut m,o) = len ((W .cut m,n) .append (W .cut n,o)) ) ; :: thesis: for x being Nat st x in dom ((W .cut m,n) .append (W .cut n,o)) holds
((W .cut m,n) .append (W .cut n,o)) . x = (W .cut m,o) . x
let x be Nat; :: thesis: ( x in dom ((W .cut m,n) .append (W .cut n,o)) implies ((W .cut m,n) .append (W .cut n,o)) . x = (W .cut m,o) . x )
assume x in dom ((W .cut m,n) .append (W .cut n,o)) ; :: thesis: ((W .cut m,n) .append (W .cut n,o)) . x = (W .cut m,o) . x
then A8: ( 1 <= x & x <= len ((W .cut m,n) .append (W .cut n,o)) ) by FINSEQ_3:27;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:18;
xaa1 < (len ((W .cut m,n) .append (W .cut n,o))) - 0 by A8, XREAL_1:17;
then A9: (W .cut m,o) . (xaa1 + 1) = W . (m + xaa1) by A1, A2, A7, Lm15;

now

per cases ( x <= len (W .cut m,n) or x > len (W .cut m,n) ) ;

suppose A10: x <= len (W .cut m,n) ; :: thesis: ((W .cut m,n) .append (W .cut n,o)) . x = (W .cut m,o) . x

then A11: xaa1 < (len (W .cut m,n)) - 0 by XREAL_1:17;
x in dom (W .cut m,n) by A8, A10, FINSEQ_3:27;
hence ((W .cut m,n) .append (W .cut n,o)) . x = (W .cut m,n) . (xaa1 + 1) by Lm12
.= (W .cut m,o) . x by A1, A2, A9, A11, Lm15 ;
:: thesis: verum

end;

suppose x > len (W .cut m,n) ; :: thesis: ((W .cut m,n) .append (W .cut n,o)) . x = (W .cut m,o) . x

then consider k being Nat such that
A12: (len (W .cut m,n)) + k = x by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
((len (W .cut m,n)) + k) + 1 <= (len (W .cut m,o)) + 1 by A7, A8, A12, XREAL_1:9;
then ((k + 1) + (len (W .cut m,n))) - (len (W .cut m,n)) <= ((len (W .cut n,o)) + (len (W .cut m,n))) - (len (W .cut m,n)) by A4, A5, A6, XREAL_1:15;
then A13: (k + 1) - 1 < ((len (W .cut n,o)) + 1) - 1 by NAT_1:13;
then ((W .cut m,n) .append (W .cut n,o)) . x = (W .cut n,o) . (k + 1) by A3, A12, Lm13
.= W . (n + k) by A1, A13, Lm15 ;
hence ((W .cut m,n) .append (W .cut n,o)) . x = (W .cut m,o) . x by A4, A9, A12; :: thesis: verum

end;

end;

end;

hence ((W .cut m,n) .append (W .cut n,o)) . x = (W .cut m,o) . x ; :: thesis: verum

end;

hence (W .cut m,n) .append (W .cut n,o) = W .cut m,o by FINSEQ_2:10; :: thesis: verum