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 that
A1: m <= n and
A2: n <= o and
A3: o <= len W ; :: thesis: (W .cut m,n) .append (W .cut n,o) = W .cut m,o
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);
A4: n <= len W by A2, A3, XXREAL_0:2;
A5: m <= o by A1, A2, XXREAL_0:2;

now

A6: (len (W .cut m,o)) + m = o + 1 by A3, A5, Lm15;
A7: (W .cut m,n) .last() = W . n by A1, A4, Lm16
.= (W .cut n,o) .first() by A2, A3, Lm16 ;
A8: (len (W .cut m,n)) + m = n + 1 by A1, A4, Lm15;
A9: (len (W .cut n,o)) + n = o + 1 by A2, A3, Lm15;
then ((len (W .cut m,n)) + (len (W .cut n,o))) + m = (1 + (len (W .cut m,o))) + m by A8, A6;
then A10: (len ((W .cut m,n) .append (W .cut n,o))) + 1 = (len (W .cut m,o)) + 1 by A7, 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 A11: 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 A12: 1 <= x by FINSEQ_3:27;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:18;
A13: x <= len ((W .cut m,n) .append (W .cut n,o)) by A11, FINSEQ_3:27;
then xaa1 < (len ((W .cut m,n) .append (W .cut n,o))) - 0 by XREAL_1:17;
then A14: (W .cut m,o) . (xaa1 + 1) = W . (m + xaa1) by A3, A5, A10, Lm15;

now

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

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

then A16: xaa1 < (len (W .cut m,n)) - 0 by XREAL_1:17;
x in dom (W .cut m,n) by A12, A15, 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, A4, A14, A16, 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
A17: (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 A10, A13, A17, 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 A8, A9, A6, XREAL_1:15;
then A18: (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 A7, A17, Lm13
.= W . (n + k) by A2, A3, A18, Lm15 ;
hence ((W .cut m,n) .append (W .cut n,o)) . x = (W .cut m,o) . x by A8, A14, A17; :: 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