let R, S be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive 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

P is RingEpimorphism by A1, QUOFIELD:def 24;
then A3: rng P = the carrier of S by QUOFIELD:def 22;
let I be Ideal of S; :: thesis: I is finitely_generated
P is RingMonomorphism by A1, QUOFIELD:def 24;
then A4: P is one-to-one by QUOFIELD:def 23;
reconsider PI = (P " ) .: I as Ideal of R by A1, Th22, Th25;
PI is finitely_generated by A2, IDEAL_1:def 27;
then consider F being non empty finite Subset of R such that
A5: (P " ) .: I = F -Ideal by IDEAL_1:def 26;
P is RingEpimorphism by A1, QUOFIELD:def 24;
then rng P = the carrier of S by QUOFIELD:def 22;
then P " = P " by A4, TOPS_2:def 4;
then P .: ((P " ) .: I) = P .: (P " I) by A4, FUNCT_1:155;
then P .: ((P " ) .: I) = I by A3, FUNCT_1:147;
then I = (P .: F) -Ideal by A1, A5, Th26;
hence I is finitely_generated ; :: thesis: verum

end;

hence S is Noetherian by IDEAL_1:def 27; :: thesis: verum