Comment by Jasper_

For a[i] to be valid, i has to be < a.length. This invariant is never invalidated during the loop body itself.