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 Th33;
hence Polynom-Ring (n,F) is Noetherian by Th32; :: thesis: verum