Description: Value of the sequence builder function at a successor, deduction form. (Contributed by Mario Carneiro, 30-Apr-2014) (Revised by AV, 3-May-2024)