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 :: thesis: W .remove (1,m) = W .cut (m,(len W))
per cases ( ( m is odd & m <= len W ) or not m is odd or not m <= len W ) ;
suppose A2: ( m is odd & m <= len W ) ; :: thesis: W .remove (1,m) = W .cut (m,(len W))
then 1 <= m by ABIAN:12;
then A3: W .remove (1,m) = (W .cut (1,1)) .append (W .cut (m,(len W))) by ;
A4: 1 <= len W by ABIAN:12;
then A5: (W .cut (1,1)) .last() = W . m by
.= (W .cut (m,(len W))) .first() by ;
A6: now :: thesis: for n being Nat st 1 <= n & n <= len (W .remove (1,m)) holds
(W .remove (1,m)) . n = (W .cut (m,(len W))) . n
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 that
A7: 1 <= n and
A8: n <= len (W .remove (1,m)) ; :: thesis: (W .remove (1,m)) . n = (W .cut (m,(len W))) . n
A9: n in dom (W .remove (1,m)) by ;
now :: thesis: (W .remove (1,m)) . n = (W .cut (m,(len W))) . n
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, A9, Lm14;
suppose A10: n in dom (W .cut (1,1)) ; :: thesis: (W .remove (1,m)) . n = (W .cut (m,(len W))) . n
then n <= len (W .cut (1,1)) by FINSEQ_3:25;
then A11: n <= 1 by ;
A12: 1 <= n by ;
then A13: n = 1 by ;
(W .remove (1,m)) . n = (W .cut (1,1)) . n by
.= <*()*> . 1 by
.= W .vertexAt 1 by FINSEQ_1:def 8
.= W . m by
.= (W .cut (m,(len W))) .first() by
.= (W .cut (m,(len W))) . 1 ;
hence (W .remove (1,m)) . n = (W .cut (m,(len W))) . n by ; :: 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
A14: k < len (W .cut (m,(len W))) and
A15: n = (len (W .cut (1,1))) + k ;
n = k + 1 by ;
hence (W .remove (1,m)) . n = (W .cut (m,(len W))) . n by A3, A5, A14, A15, Lm13; :: thesis: verum
end;
end;
end;
hence (W .remove (1,m)) . n = (W .cut (m,(len W))) . n ; :: thesis: verum
end;
(len (W .remove (1,m))) + 1 = (len (W .cut (1,1))) + (len (W .cut (m,(len W)))) by A3, A5, Lm9;
then (len (W .remove (1,m))) + 1 = (len (W .cut (m,(len W)))) + 1 by ;
hence W .remove (1,m) = W .cut (m,(len W)) by ; :: thesis: verum
end;
suppose A16: ( not m is odd 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 ; :: thesis: verum
end;
end;
end;
hence W .remove (1,m) = W .cut (m,(len W)) ; :: thesis: verum