Пусть F — идеал в R[x] (мы здесь будем считать R коммутативным, для некоммутативных колец всё доказательство сохраняется, необходимо только считать все идеалы левыми), а p — множество старших коэффициентов многочленов, принадлежащих этому идеалу. Докажем, что p — идеал.
В самом деле, если a и b — элементы p, то a и b являются старшими коэффициентами некоторых многочленов из F — f(x) = axn + … и g(x) = bxm + … Если, например, m ⩾ n, то a + b является старшим коэффициентом многочлена xm-nf(x) + g(x), принадлежащего F. Если a является старшим коэффициентом f(x) то ar является старшим коэффициентом rf(x) из идеала F для любого элемента кольца r. Таким образом p — идеал, а так как R — нётерово кольцо, то p конечно порождается некоторыми элементами a1, a2 … an, являющимися соответственно старшими коэффициентами многочленов f1, f2 … fn из F. Пусть наибольшая степень этих многочленов равна r. Можно считать что степень каждого из этих многочленов равна r (если она равна m ⩽ r, то можно сделать её такой, домножая на xr-m).
Аналогично доказывается что pk — множество старших коэффициентов многочленов из F, степень которых равна k, объединённое с нулём кольца — является идеалом, и, в силу нётеровости, конечно порождается элементами ak1, ak2 …. Пусть они являются старшими коэффициентами многочленов fk1, fk2 … степени k из идеала F.
Докажем, что многочлены f1, …, fi, …, f11, …, f1i, …, fr-11, …, fr-1i … порождают идеал F. Пусть f(x) = axs + … — какой-нибудь многочлен идеала F, тогда a принадлежит p. Если его степень s ⩾ r, то так как a по доказанному является линейной комбинацией a = r1a1 + r2a2 + …rnan старших членов многочленов f1, f2 … fn степени r , то мы получим, что f(x) − r1xs−rf1 − r2xs-rf2 − … − rnxs−rfn будет многочленом степени, меньшей, чем s и также принадлежащим идеалу F. Повторяя при необходимости эту операцию несколько раз можно прийти к многочлену степени ⩽ r.
Для многочлена степени ⩽ r применяется та же процедура, но с использованием многочленов fk1, fk2 … старшие коэффициенты которых порождают идеал pk. Далее процедура повторяется, пока мы не придем к нулевому многочлену.
Последовательно применяя теорему, можно доказать, что кольцо многочленов от n переменных R[x1, …, xn] нётерово.