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