let R, S be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for P being Function of R,S st P is RingIsomorphism & R is Noetherian holds

S is Noetherian

let P be Function of R,S; :: thesis: ( P is RingIsomorphism & R is Noetherian implies S is Noetherian )

assume that

A1: P is RingIsomorphism and

A2: R is Noetherian ; :: thesis: S is Noetherian

S is Noetherian

let P be Function of R,S; :: thesis: ( P is RingIsomorphism & R is Noetherian implies S is Noetherian )

assume that

A1: P is RingIsomorphism and

A2: R is Noetherian ; :: thesis: S is Noetherian

now :: thesis: for I being Ideal of S holds I is finitely_generated

hence
S is Noetherian
; :: thesis: verum
P is RingEpimorphism
by A1;

then A3: P is onto ;

let I be Ideal of S; :: thesis: I is finitely_generated

P is RingMonomorphism by A1;

then A4: P is one-to-one ;

reconsider PI = (P ") .: I as Ideal of R by A1, Th22, Th25;

PI is finitely_generated by A2;

then consider F being non empty finite Subset of R such that

A5: (P ") .: I = F -Ideal ;

P is onto by A3;

then P " = P " by A4, TOPS_2:def 4;

then P .: ((P ") .: I) = P .: (P " I) by A4, FUNCT_1:85;

then P .: ((P ") .: I) = I by A3, FUNCT_1:77;

then I = (P .: F) -Ideal by A1, A5, Th26;

hence I is finitely_generated ; :: thesis: verum

end;then A3: P is onto ;

let I be Ideal of S; :: thesis: I is finitely_generated

P is RingMonomorphism by A1;

then A4: P is one-to-one ;

reconsider PI = (P ") .: I as Ideal of R by A1, Th22, Th25;

PI is finitely_generated by A2;

then consider F being non empty finite Subset of R such that

A5: (P ") .: I = F -Ideal ;

P is onto by A3;

then P " = P " by A4, TOPS_2:def 4;

then P .: ((P ") .: I) = P .: (P " I) by A4, FUNCT_1:85;

then P .: ((P ") .: I) = I by A3, FUNCT_1:77;

then I = (P .: F) -Ideal by A1, A5, Th26;

hence I is finitely_generated ; :: thesis: verum