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 .remove (m,n) = W2 .remove (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 .remove (m,n) = W2 .remove (m,n)

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

W1 .remove (m,n) = W2 .remove (m,n)

let m, n be Element of NAT ; :: thesis: ( W1 = W2 implies W1 .remove (m,n) = W2 .remove (m,n) )

assume A1: W1 = W2 ; :: thesis: W1 .remove (m,n) = W2 .remove (m,n)

for W2 being Walk of G2

for m, n being Element of NAT st W1 = W2 holds

W1 .remove (m,n) = W2 .remove (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 .remove (m,n) = W2 .remove (m,n)

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

W1 .remove (m,n) = W2 .remove (m,n)

let m, n be Element of NAT ; :: thesis: ( W1 = W2 implies W1 .remove (m,n) = W2 .remove (m,n) )

assume A1: W1 = W2 ; :: thesis: W1 .remove (m,n) = W2 .remove (m,n)

now :: thesis: W1 .remove (m,n) = W2 .remove (m,n)end;

hence
W1 .remove (m,n) = W2 .remove (m,n)
; :: thesis: verumper cases
( ( m is odd & n is odd & m <= n & n <= len W1 & W1 . m = W1 . n ) or not m is odd or not n is odd or not m <= n or not n <= len W1 or not W1 . m = W1 . n )
;

end;

suppose A2:
( m is odd & n is odd & m <= n & n <= len W1 & W1 . m = W1 . n )
; :: thesis: W1 .remove (m,n) = W2 .remove (m,n)

A3:
W1 .cut (n,(len W1)) = W2 .cut (n,(len W2))
by A1, Th46;

A4: W1 .cut (1,m) = W2 .cut (1,m) by A1, Th46;

W1 .remove (m,n) = (W1 .cut (1,m)) .append (W1 .cut (n,(len W1))) by A2, Def12;

then W1 .remove (m,n) = (W2 .cut (1,m)) .append (W2 .cut (n,(len W2))) by A4, A3, Th33;

hence W1 .remove (m,n) = W2 .remove (m,n) by A1, A2, Def12; :: thesis: verum

end;A4: W1 .cut (1,m) = W2 .cut (1,m) by A1, Th46;

W1 .remove (m,n) = (W1 .cut (1,m)) .append (W1 .cut (n,(len W1))) by A2, Def12;

then W1 .remove (m,n) = (W2 .cut (1,m)) .append (W2 .cut (n,(len W2))) by A4, A3, Th33;

hence W1 .remove (m,n) = W2 .remove (m,n) by A1, A2, Def12; :: thesis: verum