let F be Field; :: thesis: for n being Element of NAT holds Polynom-Ring (n,F) is Noetherian
let n be Element of NAT ; :: thesis: Polynom-Ring (n,F) is Noetherian
F is Noetherian by Th34;
hence Polynom-Ring (n,F) is Noetherian by Th33; :: thesis: verum