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

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