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))

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))end;

hence
W .remove (1,m) = W .cut (m,(len W))
; :: thesis: verumper cases
( ( m is odd & m <= len W ) or not m is odd or not m <= len W )
;

end;

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 ;

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;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

(len (W .remove (1,m))) + 1 = (len (W .cut (1,1))) + (len (W .cut (m,(len W))))
by A3, A5, Lm9;(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;

end;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))) . nend;

hence
(W .remove (1,m)) . n = (W .cut (m,(len W))) . n
; :: thesis: verumper 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;

end;

( 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;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

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

( 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;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

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