let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; :: thesis: ( R is Noetherian implies for n being Nat holds Polynom-Ring (n,R) is Noetherian )
assume A1: R is Noetherian ; :: thesis: for n being Nat holds Polynom-Ring (n,R) is Noetherian
defpred S₁[ Nat] means Polynom-Ring ($1,R) is Noetherian ;

A2: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
ex P being Function of (Polynom-Ring (Polynom-Ring (k,R))),(Polynom-Ring ((k + 1),R)) st P is RingIsomorphism by Th31;
hence S₁[k + 1] by A3, Th27; :: thesis: verum

end;

ex P being Function of R,(Polynom-Ring (0,R)) st P is RingIsomorphism by Th28;
then A4: S₁[ 0 ] by A1, Th27;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A2); :: thesis: verum