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_{1}[ Nat] means Polynom-Ring ($1,R) is Noetherian ;

then A4: S_{1}[ 0 ]
by A1, Th27;

thus for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A4, A2); :: thesis: verum

assume A1: R is Noetherian ; :: thesis: for n being Nat holds Polynom-Ring (n,R) is Noetherian

defpred S

A2: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

ex P being Function of R,(Polynom-Ring (0,R)) st P is RingIsomorphism
by Th28;S

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[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_{1}[k + 1]
by A3, Th27; :: thesis: verum

end;assume A3: S

ex P being Function of (Polynom-Ring (Polynom-Ring (k,R))),(Polynom-Ring ((k + 1),R)) st P is RingIsomorphism by Th31;

hence S

then A4: S

thus for n being Nat holds S