let G1, G2 be _Graph; 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; 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; 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 ; ( W1 = W2 implies W1 .remove (m,n) = W2 .remove (m,n) )
assume A1:
W1 = W2
; W1 .remove (m,n) = W2 .remove (m,n)
now W1 .remove (m,n) = W2 .remove (m,n)per 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 )
;
suppose A2:
(
m is
odd &
n is
odd &
m <= n &
n <= len W1 &
W1 . m = W1 . n )
;
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;
verum end;
hence
W1 .remove (m,n) = W2 .remove (m,n)
; verum