let R be Ring; :: thesis: for S being R -isomorphic Ring
for f being Isomorphism of R,S holds
( f " is additive & f " is multiplicative & f " is unity-preserving & f " is isomorphism )
let S be R -isomorphic Ring; :: thesis: for f being Isomorphism of R,S holds
( f " is additive & f " is multiplicative & f " is unity-preserving & f " is isomorphism )
let f be Isomorphism of R,S; :: thesis: ( f " is additive & f " is multiplicative & f " is unity-preserving & f " is isomorphism )
set g = f " ;
A1: rng f = the carrier of S by FUNCT_2:def 3;

now :: thesis: for a, b being Element of S holds ((f ") . a) + ((f ") . b) = (f ") . (a + b)

let a, b be Element of S; :: thesis: ((f ") . a) + ((f ") . b) = (f ") . (a + b)
consider x being object such that
A2: ( x in the carrier of R & a = f . x ) by A1, FUNCT_2:11;
reconsider x = x as Element of R by A2;
consider y being object such that
A3: ( y in the carrier of R & b = f . y ) by A1, FUNCT_2:11;
reconsider y = y as Element of R by A3;
thus ((f ") . a) + ((f ") . b) = x + ((f ") . (f . y)) by A2, A3, FUNCT_2:26
.= x + y by FUNCT_2:26
.= (f ") . (f . (x + y)) by FUNCT_2:26
.= (f ") . (a + b) by A2, A3, VECTSP_1:def 20 ; :: thesis: verum

end;

hence A4: f " is additive ; :: thesis: ( f " is multiplicative & f " is unity-preserving & f " is isomorphism )

now :: thesis: for a, b being Element of S holds ((f ") . a) * ((f ") . b) = (f ") . (a * b)

let a, b be Element of S; :: thesis: ((f ") . a) * ((f ") . b) = (f ") . (a * b)
consider x being object such that
A5: ( x in the carrier of R & a = f . x ) by A1, FUNCT_2:11;
reconsider x = x as Element of R by A5;
consider y being object such that
A6: ( y in the carrier of R & b = f . y ) by A1, FUNCT_2:11;
reconsider y = y as Element of R by A6;
thus ((f ") . a) * ((f ") . b) = x * ((f ") . (f . y)) by A5, A6, FUNCT_2:26
.= x * y by FUNCT_2:26
.= (f ") . (f . (x * y)) by FUNCT_2:26
.= (f ") . (a * b) by A5, A6, GROUP_6:def 6 ; :: thesis: verum

end;

hence A7: f " is multiplicative ; :: thesis: ( f " is unity-preserving & f " is isomorphism )
1. R = (f ") . (f . (1_ R)) by FUNCT_2:26
.= (f ") . (1_ S) by GROUP_1:def 13
.= (f ") . (1. S) ;
hence A8: f " is unity-preserving ; :: thesis: f " is isomorphism

now :: thesis: for x being object holds
( x in rng (f ") iff x in the carrier of R )

let x be object ; :: thesis: ( x in rng (f ") iff x in the carrier of R )

now :: thesis: ( x in the carrier of R implies x in rng (f ") )

assume x in the carrier of R ; :: thesis: x in rng (f ")
then reconsider x1 = x as Element of R ;
f . x1 in the carrier of S ;
then A9: f . x1 in dom (f ") by FUNCT_2:def 1;
(f ") . (f . x1) = x1 by FUNCT_2:26;
hence x in rng (f ") by A9, FUNCT_1:def 3; :: thesis: verum

end;

hence ( x in rng (f ") iff x in the carrier of R ) ; :: thesis: verum

end;

then f " is onto by FUNCT_2:def 3, TARSKI:2;
hence f " is isomorphism by A8, A4, A7; :: thesis: verum