 Then by recursion (using the axiom of dependent choice) there is a sequence formula_15 of polynomials such that if formula_16 is the left ideal generated by formula_17 then formula_18 is of minimal degree.It is clear that formula_19 is a non-decreasing sequence of naturals.Let formula_20 be the leading coefficient of formula_21 and let formula_22 be the left ideal in formula_1 generated by formula_24.