Round-six lemma `vStep_fsp`