theorem Th11: :: MATGRP_0:4

for R1, R2 being Ring
for phi being Function of R1,R2 st phi is isomorphism holds
for x being Element of R1 st phi . x = 1. R2 holds
x = 1. R1