for R, S being non empty doubleLoopStr
for P being Function of R,S st P is RingIsomorphism holds
P " is RingIsomorphism