let G be _Graph; :: thesis: for W being Walk of G
for m being Element of NAT st W .first() = W . m holds
W .remove 1,m = W .cut m,(len W)
let W be Walk of G; :: thesis: for m being Element of NAT st W .first() = W . m holds
W .remove 1,m = W .cut m,(len W)
let m be Element of NAT ; :: thesis: ( W .first() = W . m implies W .remove 1,m = W .cut m,(len W) )
assume A1: W .first() = W . m ; :: thesis: W .remove 1,m = W .cut m,(len W)

now

per cases ( ( not m is even & m <= len W ) or m is even or not m <= len W ) ;

suppose A2: ( not m is even & m <= len W ) ; :: thesis: W .remove 1,m = W .cut m,(len W)

then ( not 1 is even & 1 <= m ) by HEYTING3:1, JORDAN12:3;
then A3: W .remove 1,m = (W .cut 1,1) .append (W .cut m,(len W)) by A1, A2, Def12;
A4: 1 <= len W by HEYTING3:1;
then A5: (W .cut 1,1) .last() = W . m by A1, Lm16, JORDAN12:3
.= (W .cut m,(len W)) .first() by A2, Lm16 ;
then (len (W .remove 1,m)) + 1 = (len (W .cut 1,1)) + (len (W .cut m,(len W))) by A3, Lm9;
then A6: (len (W .remove 1,m)) + 1 = (len (W .cut m,(len W))) + 1 by Lm22, HEYTING3:1, JORDAN12:3;

now

let n be Nat; :: thesis: ( 1 <= n & n <= len (W .remove 1,m) implies (W .remove 1,m) . n = (W .cut m,(len W)) . n )
assume ( 1 <= n & n <= len (W .remove 1,m) ) ; :: thesis: (W .remove 1,m) . n = (W .cut m,(len W)) . n
then A7: n in dom (W .remove 1,m) by FINSEQ_3:27;

now

per cases ( n in dom (W .cut 1,1) or ex k being Element of NAT st
( k < len (W .cut m,(len W)) & n = (len (W .cut 1,1)) + k ) ) by A3, A7, Lm14;

suppose A8: n in dom (W .cut 1,1) ; :: thesis: (W .remove 1,m) . n = (W .cut m,(len W)) . n

then A9: ( 1 <= n & n <= len (W .cut 1,1) ) by FINSEQ_3:27;
then A10: n <= 1 by A4, Lm22, JORDAN12:3;
then A11: n = 1 by A9, XXREAL_0:1;
(W .remove 1,m) . n = (W .cut 1,1) . n by A3, A8, Lm12
.= <*(W .vertexAt 1)*> . 1 by A4, A11, Lm19, JORDAN12:3
.= W .vertexAt 1 by FINSEQ_1:def 8
.= W . m by A1, A4, Def8, JORDAN12:3
.= (W .cut m,(len W)) .first() by A2, Lm16
.= (W .cut m,(len W)) . 1 ;
hence (W .remove 1,m) . n = (W .cut m,(len W)) . n by A9, A10, XXREAL_0:1; :: thesis: verum

end;

suppose ex k being Element of NAT st
( k < len (W .cut m,(len W)) & n = (len (W .cut 1,1)) + k ) ; :: thesis: (W .remove 1,m) . n = (W .cut m,(len W)) . n

then consider k being Element of NAT such that
A12: ( k < len (W .cut m,(len W)) & n = (len (W .cut 1,1)) + k ) ;
n = k + 1 by A12, Lm22, HEYTING3:1, JORDAN12:3;
hence (W .remove 1,m) . n = (W .cut m,(len W)) . n by A3, A5, A12, Lm13; :: thesis: verum

end;

end;

end;

hence (W .remove 1,m) . n = (W .cut m,(len W)) . n ; :: thesis: verum

end;

hence W .remove 1,m = W .cut m,(len W) by A6, FINSEQ_1:18; :: thesis: verum

end;

suppose A13: ( m is even or not m <= len W ) ; :: thesis: W .remove 1,m = W .cut m,(len W)

then W .cut m,(len W) = W by Def11;
hence W .remove 1,m = W .cut m,(len W) by A13, Def12; :: thesis: verum

end;

end;

end;

hence W .remove 1,m = W .cut m,(len W) ; :: thesis: verum