let G be _Graph; :: thesis: for W1, W2 being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W1 & W1 .last() = W2 .first() holds
(W1 .append W2) .cut (m,n) = W1 .cut (m,n)

let W1, W2 be Walk of G; :: thesis: for m, n being odd Element of NAT st m <= n & n <= len W1 & W1 .last() = W2 .first() holds
(W1 .append W2) .cut (m,n) = W1 .cut (m,n)

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W1 & W1 .last() = W2 .first() implies (W1 .append W2) .cut (m,n) = W1 .cut (m,n) )
assume that
A1: m <= n and
A2: n <= len W1 and
A3: W1 .last() = W2 .first() ; :: thesis: (W1 .append W2) .cut (m,n) = W1 .cut (m,n)
A4: W1 .cut (m,n) = (m,n) -cut W1 by ;
set W3 = W1 .append W2;
len W1 <= len (W1 .append W2) by ;
then A5: n <= len (W1 .append W2) by ;
then A6: (len ((W1 .append W2) .cut (m,n))) + m = n + 1 by
.= (len (W1 .cut (m,n))) + m by A1, A2, Lm15 ;
A7: 1 <= m by ABIAN:12;
A8: (W1 .append W2) .cut (m,n) = (m,n) -cut (W1 .append W2) by ;
now :: thesis: for x being Nat st x in dom (W1 .cut (m,n)) holds
((W1 .append W2) .cut (m,n)) . x = (W1 .cut (m,n)) . x
let x be Nat; :: thesis: ( x in dom (W1 .cut (m,n)) implies ((W1 .append W2) .cut (m,n)) . x = (W1 .cut (m,n)) . x )
assume A9: x in dom (W1 .cut (m,n)) ; :: thesis: ((W1 .append W2) .cut (m,n)) . x = (W1 .cut (m,n)) . x
then 1 <= x by FINSEQ_3:25;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:5;
A10: x <= len (W1 .cut (m,n)) by ;
then A11: xaa1 < (len (W1 .cut (m,n))) - 0 by XREAL_1:15;
(len (W1 .cut (m,n))) + m = n + 1 by A1, A2, Lm15;
then m + xaa1 < n + 1 by ;
then m + xaa1 <= n by NAT_1:13;
then A12: m + xaa1 <= len W1 by ;
1 <= m + xaa1 by ;
then A13: m + xaa1 in dom W1 by ;
A14: xaa1 + 1 = x ;
xaa1 < (len ((W1 .append W2) .cut (m,n))) - 0 by ;
then A15: ((W1 .append W2) .cut (m,n)) . x = (W1 .append W2) . (m + xaa1) by ;
(W1 .cut (m,n)) . x = W1 . (m + xaa1) by ;
hence ((W1 .append W2) .cut (m,n)) . x = (W1 .cut (m,n)) . x by ; :: thesis: verum
end;
hence (W1 .append W2) .cut (m,n) = W1 .cut (m,n) by ; :: thesis: verum