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 A1: ( m <= n & n <= len W & W . m = W . n ) ; :: thesis: for x being Element of NAT st x in Seg m holds
(W .remove m,n) . x = W . x
then A2: W .remove m,n = (W .cut 1,m) .append (W .cut n,(len W)) by Def12;
let x be Element of NAT ; :: thesis: ( x in Seg m implies (W .remove m,n) . x = W . x )
assume x in Seg m ; :: thesis: (W .remove m,n) . x = W . x
then ( 1 <= x & x <= m ) by FINSEQ_1:3;
then ( 1 <= x & x <= len (W .cut 1,m) ) by A1, Lm22, XXREAL_0:2;
then A3: x in dom (W .cut 1,m) by FINSEQ_3:27;
hence (W .remove m,n) . x = (W .cut 1,m) . x by A2, Lm12
.= W . x by A1, A3, Lm23, XXREAL_0:2 ;
:: thesis: verum