let R1, R2 be Ring; :: thesis: for phi being Function of R1,R2 st phi is isomorphism holds
for psi being Function of R2,R1 st psi = phi " holds
psi is bijective
let phi be Function of R1,R2; :: thesis: ( phi is isomorphism implies for psi being Function of R2,R1 st psi = phi " holds
psi is bijective )
assume A1: phi is isomorphism ; :: thesis: for psi being Function of R2,R1 st psi = phi " holds
psi is bijective
let psi be Function of R2,R1; :: thesis: ( psi = phi " implies psi is bijective )
assume A2: psi = phi " ; :: thesis: psi is bijective
then psi * phi = id (dom phi) by A1, FUNCT_1:39
.= id the carrier of R1 by FUNCT_2:def 1 ;
then ( phi is one-to-one & psi is onto ) by FUNCT_2:23;
hence psi is bijective by A2; :: thesis: verum