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

now

per cases ( ( not m is even & not n is even & m <= n & n <= len W1 & W1 . m = W1 . n ) or m is even or n is even or not m <= n or not n <= len W1 or not W1 . m = W1 . n ) ;

suppose A2: ( not m is even & not n is even & 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, Th49;
A4: W1 .cut 1,m = W2 .cut 1,m by A1, Th49;
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, Th36;
hence W1 .remove m,n = W2 .remove m,n by A1, A2, Def12; :: thesis: verum

end;

suppose A5: ( m is even or n is even or not m <= n or not n <= len W1 or not W1 . m = W1 . n ) ; :: thesis: W1 .remove m,n = W2 .remove m,n

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

end;

end;

end;

hence W1 .remove m,n = W2 .remove m,n ; :: thesis: verum