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

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

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;

hence S is Noetherian ; :: thesis: verum