let R1, R2 be Ring; :: thesis: 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
let phi be Function of R1,R2; :: thesis: ( phi is isomorphism implies for x being Element of R1 st phi . x = 1. R2 holds
x = 1. R1 )
assume A1: phi is isomorphism ; :: thesis: for x being Element of R1 st phi . x = 1. R2 holds
x = 1. R1
let x be Element of R1; :: thesis: ( phi . x = 1. R2 implies x = 1. R1 )
assume A2: phi . x = 1. R2 ; :: thesis: x = 1. R1
( x in the carrier of R1 & dom phi = the carrier of R1 ) by FUNCT_2:def 1;
then A4: for x2 being object st x2 in dom phi & phi . x = phi . x2 holds
x2 = x by A1, FUNCT_1:def 4;
( 1. R1 in the carrier of R1 & dom phi = the carrier of R1 ) by FUNCT_2:def 1;
then A5: 1. R1 in dom phi ;
phi . (1. R1) = phi . x by A1, A2, Th1;
hence x = 1. R1 by A4, A5; :: thesis: verum