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

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:27;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:18;
A10: x <= len (W1 .cut m,n) by A9, FINSEQ_3:27;
then A11: xaa1 < (len (W1 .cut m,n)) - 0 by XREAL_1:17;
(len (W1 .cut m,n)) + m = n + 1 by A1, A2, Lm15;
then m + xaa1 < n + 1 by A11, XREAL_1:10;
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:27;
A14: xaa1 + 1 = x ;
xaa1 < (len ((W1 .append W2) .cut m,n)) - 0 by A6, A10, XREAL_1:17;
then A15: ((W1 .append W2) .cut m,n) . x = (W1 .append W2) . (m + xaa1) by A1, A5, A8, A7, A14, GRAPH_2:def 1;
(W1 .cut m,n) . x = W1 . (m + xaa1) by A1, A2, A4, A7, A14, A11, GRAPH_2:def 1;
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:10; :: thesis: verum