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 A1: ( P is RingIsomorphism & R is Noetherian ) ; :: thesis: S is Noetherian

now

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

end;

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