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 A1: ( m <= n & n <= len W1 & W1 .last() = W2 .first() ) ; :: thesis: (W1 .append W2) .cut m,n = W1 .cut m,n
set W3 = W1 .append W2;
len W1 <= len (W1 .append W2) by A1, Lm10;
then A2: n <= len (W1 .append W2) by A1, XXREAL_0:2;
then A3: (len ((W1 .append W2) .cut m,n)) + m = n + 1 by A1, Lm15
.= (len (W1 .cut m,n)) + m by A1, Lm15 ;
A4: (W1 .append W2) .cut m,n = m,n -cut (W1 .append W2) by A1, A2, Def11;
A5: W1 .cut m,n = m,n -cut W1 by A1, Def11;
A6: ( 1 <= m & m <= n ) by A1, HEYTING3:1;

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 x in dom (W1 .cut m,n) ; :: thesis: ((W1 .append W2) .cut m,n) . x = (W1 .cut m,n) . x
then x in dom (W1 .cut m,n) ;
then A7: ( 1 <= x & x <= len (W1 .cut m,n) ) by FINSEQ_3:27;
then reconsider xaa1 = x - 1 as Element of NAT by INT_1:18;
A8: xaa1 + 1 = x ;
A9: xaa1 < (len ((W1 .append W2) .cut m,n)) - 0 by A3, A7, XREAL_1:17;
A10: xaa1 < (len (W1 .cut m,n)) - 0 by A7, XREAL_1:17;
then A11: (W1 .cut m,n) . x = W1 . (m + xaa1) by A1, A5, A6, A8, GRAPH_2:def 1;
A12: ((W1 .append W2) .cut m,n) . x = (W1 .append W2) . (m + xaa1) by A2, A4, A6, A8, A9, GRAPH_2:def 1;
A13: 1 <= m + xaa1 by HEYTING3:1, NAT_1:12;
(len (W1 .cut m,n)) + m = n + 1 by A1, Lm15;
then m + xaa1 < n + 1 by A10, XREAL_1:10;
then m + xaa1 <= n by NAT_1:13;
then m + xaa1 <= len W1 by A1, XXREAL_0:2;
then m + xaa1 in dom W1 by A13, FINSEQ_3:27;
hence ((W1 .append W2) .cut m,n) . x = (W1 .cut m,n) . x by A11, A12, Lm12; :: thesis: verum

end;

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