let G be _Graph; :: thesis: for W being Walk of G holds W .cut (1,(len W)) = W
let W be Walk of G; :: thesis: W .cut (1,(len W)) = W
1 <= len W by ABIAN:12;
then W .cut (1,(len W)) = (1,(len W)) -cut W by Def11, JORDAN12:2;
hence W .cut (1,(len W)) = W by FINSEQ_6:133; :: thesis: verum