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 A1, A2, Def11;

set W3 = W1 .append W2;

len W1 <= len (W1 .append W2) by A3, Lm10;

then A5: n <= len (W1 .append W2) by A2, XXREAL_0:2;

then A6: (len ((W1 .append W2) .cut (m,n))) + m = n + 1 by A1, Lm15

.= (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 A1, A5, Def11;

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 A1, A2, Def11;

set W3 = W1 .append W2;

len W1 <= len (W1 .append W2) by A3, Lm10;

then A5: n <= len (W1 .append W2) by A2, XXREAL_0:2;

then A6: (len ((W1 .append W2) .cut (m,n))) + m = n + 1 by A1, Lm15

.= (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 A1, A5, Def11;

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

hence
(W1 .append W2) .cut (m,n) = W1 .cut (m,n)
by A6, FINSEQ_2:9; :: thesis: verum((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 A9, FINSEQ_3:25;

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 A11, XREAL_1:8;

then m + xaa1 <= n by NAT_1:13;

then A12: m + xaa1 <= len W1 by A2, XXREAL_0:2;

1 <= m + xaa1 by ABIAN:12, NAT_1:12;

then A13: m + xaa1 in dom W1 by A12, FINSEQ_3:25;

A14: xaa1 + 1 = x ;

xaa1 < (len ((W1 .append W2) .cut (m,n))) - 0 by A6, A10, XREAL_1:15;

then A15: ((W1 .append W2) .cut (m,n)) . x = (W1 .append W2) . (m + xaa1) by A1, A5, A8, A7, A14, FINSEQ_6:def 4;

(W1 .cut (m,n)) . x = W1 . (m + xaa1) by A1, A2, A4, A7, A14, A11, FINSEQ_6:def 4;

hence ((W1 .append W2) .cut (m,n)) . x = (W1 .cut (m,n)) . x by A15, A13, Lm12; :: thesis: verum

end;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 A9, FINSEQ_3:25;

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 A11, XREAL_1:8;

then m + xaa1 <= n by NAT_1:13;

then A12: m + xaa1 <= len W1 by A2, XXREAL_0:2;

1 <= m + xaa1 by ABIAN:12, NAT_1:12;

then A13: m + xaa1 in dom W1 by A12, FINSEQ_3:25;

A14: xaa1 + 1 = x ;

xaa1 < (len ((W1 .append W2) .cut (m,n))) - 0 by A6, A10, XREAL_1:15;

then A15: ((W1 .append W2) .cut (m,n)) . x = (W1 .append W2) . (m + xaa1) by A1, A5, A8, A7, A14, FINSEQ_6:def 4;

(W1 .cut (m,n)) . x = W1 . (m + xaa1) by A1, A2, A4, A7, A14, A11, FINSEQ_6:def 4;

hence ((W1 .append W2) .cut (m,n)) . x = (W1 .cut (m,n)) . x by A15, A13, Lm12; :: thesis: verum