let R be non empty 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