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

A2: now

let k be Element of 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 Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A2); :: thesis: verum