let G be _Graph; :: thesis: for W being Walk of G

for x, y being set

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st x in Seg m holds

(W .remove (m,n)) . x = W . x

let W be Walk of G; :: thesis: for x, y being set

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st x in Seg m holds

(W .remove (m,n)) . x = W . x

let x, y be set ; :: thesis: for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st x in Seg m holds

(W .remove (m,n)) . x = W . x

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W & W . m = W . n implies for x being Element of NAT st x in Seg m holds

(W .remove (m,n)) . x = W . x )

set W2 = W .remove (m,n);

assume that

A1: m <= n and

A2: n <= len W and

A3: W . m = W . n ; :: thesis: for x being Element of NAT st x in Seg m holds

(W .remove (m,n)) . x = W . x

let x be Element of NAT ; :: thesis: ( x in Seg m implies (W .remove (m,n)) . x = W . x )

assume A4: x in Seg m ; :: thesis: (W .remove (m,n)) . x = W . x

then x <= m by FINSEQ_1:1;

then A5: x <= len (W .cut (1,m)) by A1, A2, Lm22, XXREAL_0:2;

1 <= x by A4, FINSEQ_1:1;

then A6: x in dom (W .cut (1,m)) by A5, FINSEQ_3:25;

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

hence (W .remove (m,n)) . x = (W .cut (1,m)) . x by A6, Lm12

.= W . x by A1, A2, A6, Lm23, XXREAL_0:2 ;

:: thesis: verum

for x, y being set

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st x in Seg m holds

(W .remove (m,n)) . x = W . x

let W be Walk of G; :: thesis: for x, y being set

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st x in Seg m holds

(W .remove (m,n)) . x = W . x

let x, y be set ; :: thesis: for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st x in Seg m holds

(W .remove (m,n)) . x = W . x

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W & W . m = W . n implies for x being Element of NAT st x in Seg m holds

(W .remove (m,n)) . x = W . x )

set W2 = W .remove (m,n);

assume that

A1: m <= n and

A2: n <= len W and

A3: W . m = W . n ; :: thesis: for x being Element of NAT st x in Seg m holds

(W .remove (m,n)) . x = W . x

let x be Element of NAT ; :: thesis: ( x in Seg m implies (W .remove (m,n)) . x = W . x )

assume A4: x in Seg m ; :: thesis: (W .remove (m,n)) . x = W . x

then x <= m by FINSEQ_1:1;

then A5: x <= len (W .cut (1,m)) by A1, A2, Lm22, XXREAL_0:2;

1 <= x by A4, FINSEQ_1:1;

then A6: x in dom (W .cut (1,m)) by A5, FINSEQ_3:25;

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

hence (W .remove (m,n)) . x = (W .cut (1,m)) . x by A6, Lm12

.= W . x by A1, A2, A6, Lm23, XXREAL_0:2 ;

:: thesis: verum