命題
K を可換体とする。
H/K を拡大（過去スレpart4の512）とする。
K[X_1、．．．、X_n] を多項式環とする。
α_1、．．．、α_n を H の元の有限列とする。
α_1、．．．、α_n が K 上代数的独立（>>2）であるためには
f(X_1、．．．、X_n) ∈ K[X_1、．．．、X_n] で f(α_1、．．．、α_n) = 0 なら
常に f(X_1、．．．、X_n) = 0 となることが必要十分である。

証明
自明である。