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)
now :: thesis: W .remove (m,(len W)) = W .cut (1,m)
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 (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;
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
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;
hence W .remove (m,(len W)) = W .cut (1,m) by A4, FINSEQ_1:14; :: thesis: verum
end;
suppose A8: ( not m is odd or not m <= len W ) ; :: thesis: W .remove (m,(len W)) = W .cut (1,m)
then W .cut (1,m) = W by Def11;
hence W .remove (m,(len W)) = W .cut (1,m) by A8, Def12; :: thesis: verum
end;
end;
end;
hence W .remove (m,(len W)) = W .cut (1,m) ; :: thesis: verum