let R, S be Ring; :: thesis: ( R == S iff ex f being Function of R,S st
( f = id R & f is isomorphism ) )

A: now :: thesis: ( R == S implies ex f being Function of R,S st
( f = id R & f is isomorphism ) )

assume B0: R == S ; :: thesis: ex f being Function of R,S st
( f = id R & f is isomorphism )
thus ex f being Function of R,S st
( f = id R & f is isomorphism ) :: thesis: verum

proof

reconsider f = id R as Function of R,S by B0;
take f ; :: thesis: ( f = id R & f is isomorphism )
( f is additive & f is multiplicative & f is unity-preserving ) by B0;
hence ( f = id R & f is isomorphism ) by B0; :: thesis: verum

end;

end;

now :: thesis: ( ex f being Function of R,S st
( f = id R & f is isomorphism ) implies R == S )

assume ex f being Function of R,S st
( f = id R & f is isomorphism ) ; :: thesis: R == S
then consider f being Function of R,S such that
B0: ( f = id R & f is isomorphism ) ;

B1: now :: thesis: for o being object st o in the carrier of R holds
o in the carrier of S

let o be object ; :: thesis: ( o in the carrier of R implies o in the carrier of S )
assume o in the carrier of R ; :: thesis: o in the carrier of S
then reconsider a = o as Element of R ;
f . a in the carrier of S ;
hence o in the carrier of S by B0; :: thesis: verum

end;

BB: now :: thesis: for o being object st o in the carrier of S holds
o in the carrier of R

let o be object ; :: thesis: ( o in the carrier of S implies o in the carrier of R )
assume B2: o in the carrier of S ; :: thesis: o in the carrier of R
rng f = the carrier of S by B0, FUNCT_2:def 3;
hence o in the carrier of R by B2, B0; :: thesis: verum

end;

then B2: the carrier of S = the carrier of R by B1, TARSKI:2;
H: ( f is additive & f is multiplicative & f is unity-preserving ) by B0;
B4: 0. S = f . (0. R) by B0, RING_2:6
.= 0. R by B0 ;

now :: thesis: for x being object st x in [: the carrier of R, the carrier of R:] holds
the addF of R . x = the addF of S . x

let x be object ; :: thesis: ( x in [: the carrier of R, the carrier of R:] implies the addF of R . x = the addF of S . x )
assume x in [: the carrier of R, the carrier of R:] ; :: thesis: the addF of R . x = the addF of S . x
then consider a, b being object such that
B5: ( a in the carrier of R & b in the carrier of R & x = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of R by B5;
thus the addF of R . x = f . (a + b) by B5, B0
.= (f . a) + (f . b) by H
.= the addF of S . x by B0, B5 ; :: thesis: verum

end;

then B5: the addF of R = the addF of S by B2;

now :: thesis: for x being object st x in [: the carrier of R, the carrier of R:] holds
the multF of R . x = the multF of S . x

let x be object ; :: thesis: ( x in [: the carrier of R, the carrier of R:] implies the multF of R . x = the multF of S . x )
assume x in [: the carrier of R, the carrier of R:] ; :: thesis: the multF of R . x = the multF of S . x
then consider a, b being object such that
B5: ( a in the carrier of R & b in the carrier of R & x = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of R by B5;
thus the multF of R . x = f . (a * b) by B5, B0
.= (f . a) * (f . b) by H
.= the multF of S . x by B0, B5 ; :: thesis: verum

end;

then the multF of R = the multF of S by B2;
hence R == S by B1, BB, TARSKI:2, H, B0, B4, B5; :: thesis: verum

end;

hence ( R == S iff ex f being Function of R,S st
( f = id R & f is isomorphism ) ) by A; :: thesis: verum