let R1, R2 be Ring; :: thesis: ( R1,R2 are_isomorphic implies ( R2 is R1 -isomorphic & R1 is R2 -isomorphic ) )
assume R1,R2 are_isomorphic ; :: thesis: ( R2 is R1 -isomorphic & R1 is R2 -isomorphic )
then consider f being Function of R1,R2 such that
A1: f is RingIsomorphism by QUOFIELD:def 23;
thus R2 is R1 -isomorphic by A1, RING_3:def 4; :: thesis: R1 is R2 -isomorphic
hence R1 is R2 -isomorphic by RING_3:74; :: thesis: verum