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;

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 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;

hence (W1 .append W2) .cut (m,n) = W1 .cut (m,n) by A6, FINSEQ_2:9; :: thesis: verum