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 A1, A2, Def12, JORDAN12:2;
A4: 1 <= len W by ABIAN:12;
then A5: (W .cut (1,1)) .last() = W . m by A1, Lm16, JORDAN12:2
.= (W .cut (m,(len W))) .first() by A2, Lm16 ;
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 A7, A8, FINSEQ_3:25;
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 A4, Lm22, JORDAN12:2;
A12: 1 <= n by A10, FINSEQ_3:25;
then A13: n = 1 by A11, XXREAL_0:1;
(W .remove (1,m)) . n = (W .cut (1,1)) . n by A3, A10, Lm12
.= <*(W .vertexAt 1)*> . 1 by A4, A13, Lm19, JORDAN12:2
.= W .vertexAt 1 by FINSEQ_1:def 8
.= W . m by A1, A4, Def8, JORDAN12:2
.= (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 A12, A11, 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
A14: k < len (W .cut (m,(len W))) and
A15: n = (len (W .cut (1,1))) + k ;
n = k + 1 by A14, A15, Lm22, ABIAN:12, JORDAN12:2;
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 Lm22, ABIAN:12, JORDAN12:2;
hence W .remove (1,m) = W .cut (m,(len W)) by A6, FINSEQ_1:14; :: 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 A16, Def12; :: thesis: verum
end;
end;
end;
hence W .remove (1,m) = W .cut (m,(len W)) ; :: thesis: verum