let G be _Graph; :: thesis: for W being Walk of G

for m being Element of NAT st W . m = W .last() holds

W .remove (m,(len W)) = W .cut (1,m)

let W be Walk of G; :: thesis: for m being Element of NAT st W . m = W .last() holds

W .remove (m,(len W)) = W .cut (1,m)

let m be Element of NAT ; :: thesis: ( W . m = W .last() implies W .remove (m,(len W)) = W .cut (1,m) )

assume A1: W . m = W .last() ; :: thesis: W .remove (m,(len W)) = W .cut (1,m)

for m being Element of NAT st W . m = W .last() holds

W .remove (m,(len W)) = W .cut (1,m)

let W be Walk of G; :: thesis: for m being Element of NAT st W . m = W .last() holds

W .remove (m,(len W)) = W .cut (1,m)

let m be Element of NAT ; :: thesis: ( W . m = W .last() implies W .remove (m,(len W)) = W .cut (1,m) )

assume A1: W . m = W .last() ; :: thesis: W .remove (m,(len W)) = W .cut (1,m)

now :: thesis: W .remove (m,(len W)) = W .cut (1,m)end;

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

then A3:
(len (W .remove (m,(len W)))) + (len W) = (len W) + m
by A1, Lm24;

then A4: len (W .remove (m,(len W))) = len (W .cut (1,m)) by A2, Lm22;

end;then A4: len (W .remove (m,(len W))) = len (W .cut (1,m)) by A2, Lm22;

now :: thesis: for k being Nat st 1 <= k & k <= len (W .remove (m,(len W))) holds

(W .remove (m,(len W))) . k = (W .cut (1,m)) . k

hence
W .remove (m,(len W)) = W .cut (1,m)
by A4, FINSEQ_1:14; :: thesis: verum(W .remove (m,(len W))) . k = (W .cut (1,m)) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (W .remove (m,(len W))) implies (W .remove (m,(len W))) . k = (W .cut (1,m)) . k )

assume that

A5: 1 <= k and

A6: k <= len (W .remove (m,(len W))) ; :: thesis: (W .remove (m,(len W))) . k = (W .cut (1,m)) . k

A7: k in dom (W .cut (1,m)) by A4, A5, A6, FINSEQ_3:25;

k in Seg m by A3, A5, A6, FINSEQ_1:1;

hence (W .remove (m,(len W))) . k = W . k by A1, A2, Lm29

.= (W .cut (1,m)) . k by A2, A7, Lm23 ;

:: thesis: verum

end;assume that

A5: 1 <= k and

A6: k <= len (W .remove (m,(len W))) ; :: thesis: (W .remove (m,(len W))) . k = (W .cut (1,m)) . k

A7: k in dom (W .cut (1,m)) by A4, A5, A6, FINSEQ_3:25;

k in Seg m by A3, A5, A6, FINSEQ_1:1;

hence (W .remove (m,(len W))) . k = W . k by A1, A2, Lm29

.= (W .cut (1,m)) . k by A2, A7, Lm23 ;

:: thesis: verum