for R being Ring
for S being b₁ -isomorphic Ring
for f being Isomorphism of R,S holds f " is Isomorphism of S,R by Lm7;