let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2
for m, n being Element of NAT st W1 = W2 holds
W1 .cut (m,n) = W2 .cut (m,n)

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2
for m, n being Element of NAT st W1 = W2 holds
W1 .cut (m,n) = W2 .cut (m,n)

let W2 be Walk of G2; :: thesis: for m, n being Element of NAT st W1 = W2 holds
W1 .cut (m,n) = W2 .cut (m,n)

let m, n be Element of NAT ; :: thesis: ( W1 = W2 implies W1 .cut (m,n) = W2 .cut (m,n) )
assume A1: W1 = W2 ; :: thesis: W1 .cut (m,n) = W2 .cut (m,n)
now :: thesis: W1 .cut (m,n) = W2 .cut (m,n)
per cases ( ( m is odd & n is odd & m <= n & n <= len W1 ) or not m is odd or not n is odd or not m <= n or not n <= len W1 ) ;
suppose A2: ( m is odd & n is odd & m <= n & n <= len W1 ) ; :: thesis: W1 .cut (m,n) = W2 .cut (m,n)
hence W1 .cut (m,n) = (m,n) -cut W2 by
.= W2 .cut (m,n) by ;
:: thesis: verum
end;
suppose A3: ( not m is odd or not n is odd or not m <= n or not n <= len W1 ) ; :: thesis: W1 .cut (m,n) = W2 .cut (m,n)
hence W1 .cut (m,n) = W2 by
.= W2 .cut (m,n) by ;
:: thesis: verum
end;
end;
end;
hence W1 .cut (m,n) = W2 .cut (m,n) ; :: thesis: verum