let R1, R2 be Ring; :: thesis: ( R1,R2 are_isomorphic implies UnitGroup R1, UnitGroup R2 are_isomorphic )
assume R1,R2 are_isomorphic ; :: thesis: UnitGroup R1, UnitGroup R2 are_isomorphic
then consider phi being Function of R1,R2 such that
A1: phi is RingIsomorphism by QUOFIELD:def 23;
set psi = phi | the carrier of (UnitGroup R1);
A2: phi | the carrier of (UnitGroup R1) is Function of (units R1),R2 by FUNCT_2:32;
then A3: dom (phi | the carrier of (UnitGroup R1)) = units R1 by FUNCT_2:def 1;

now :: thesis: for y being object st y in rng (phi | the carrier of (UnitGroup R1)) holds
y in units R2

let y be object ; :: thesis: ( y in rng (phi | the carrier of (UnitGroup R1)) implies y in units R2 )
assume y in rng (phi | the carrier of (UnitGroup R1)) ; :: thesis: y in units R2
then consider x being object such that
A4: ( x in dom (phi | the carrier of (UnitGroup R1)) & (phi | the carrier of (UnitGroup R1)) . x = y ) by FUNCT_1:def 3;
reconsider x9 = x as unital Element of R1 by A3, A4, Th107;
(phi | the carrier of (UnitGroup R1)) . x in the carrier of R2 by A2, A3, A4, FUNCT_2:5;
then reconsider y9 = y as Element of R2 by A4;
consider w being Element of R1 such that
A5: ( x9 * w = 1. R1 & w * x9 = 1. R1 ) by GCD_1:def 2;
( (phi . w) * y9 = 1. R2 & y9 * (phi . w) = 1. R2 )

proof

x9 in the carrier of (UnitGroup R1) ;
then A6: phi . x9 = y9 by A4, FUNCT_1:49;
thus 1. R2 = phi . (w * x9) by A1, A5, Th1
.= (phi . w) * y9 by A1, A6, GROUP_6:def 6 ; :: thesis: y9 * (phi . w) = 1. R2
thus 1. R2 = phi . (x9 * w) by A1, A5, Th1
.= y9 * (phi . w) by A1, A6, GROUP_6:def 6 ; :: thesis: verum

end;

then y9 is unital by GCD_1:def 2;
hence y in units R2 ; :: thesis: verum

end;

then reconsider psi = phi | the carrier of (UnitGroup R1) as Function of (UnitGroup R1),(UnitGroup R2) by A3, FUNCT_2:2, TARSKI:def 3;
A7: for x being Element of R1 st x in units R1 holds
psi . x = phi . x by FUNCT_1:49;
A8: for a being Element of (UnitGroup R1) ex x being Element of R1 st
( a = x & phi . x = psi . a )

proof

let a be Element of (UnitGroup R1); :: thesis: ex x being Element of R1 st
( a = x & phi . x = psi . a )
a in units R1 ;
then reconsider x = a as Element of R1 ;
take x ; :: thesis: ( a = x & phi . x = psi . a )
thus a = x ; :: thesis: phi . x = psi . a
thus phi . x = psi . a by FUNCT_1:49; :: thesis: verum

end;

A9: psi is one-to-one by A1, FUNCT_1:52;
for a, b being Element of (UnitGroup R1) holds psi . (a * b) = (psi . a) * (psi . b)

proof

let a, b be Element of (UnitGroup R1); :: thesis: psi . (a * b) = (psi . a) * (psi . b)
consider x being Element of R1 such that
A10: ( a = x & phi . x = psi . a ) by A8;
consider y being Element of R1 such that
A11: ( b = y & phi . y = psi . b ) by A8;
( x is unital & y is unital ) by A10, A11, Th107;
then x * y in units R1 ;
then psi . (x * y) = phi . (x * y) by A7
.= (phi . x) * (phi . y) by A1, GROUP_6:def 6
.= (psi . a) * (psi . b) by A10, A11, FUNCT_1:49, ZFMISC_1:87 ;
hence psi . (a * b) = (psi . a) * (psi . b) by A10, A11, Th110; :: thesis: verum

end;

then reconsider psi = psi as Homomorphism of (UnitGroup R1),(UnitGroup R2) by GROUP_6:def 6;
for y being object st y in the carrier of (UnitGroup R2) holds
ex x being object st
( x in the carrier of (UnitGroup R1) & y = psi . x )

proof

let y be object ; :: thesis: ( y in the carrier of (UnitGroup R2) implies ex x being object st
( x in the carrier of (UnitGroup R1) & y = psi . x ) )
assume A13: y in the carrier of (UnitGroup R2) ; :: thesis: ex x being object st
( x in the carrier of (UnitGroup R1) & y = psi . x )
then reconsider y9 = y as Element of (UnitGroup R2) ;
reconsider y0 = y as Element of R2 by A13;
A14: rng phi = the carrier of R2 by A1, FUNCT_2:def 3;
consider x0 being object such that
A15: ( x0 in dom phi & y0 = phi . x0 ) by A14, FUNCT_1:def 3;
reconsider x0 = x0 as Element of R1 by A15;
consider z0 being Element of R2 such that
A16: ( y0 * z0 = 1. R2 & z0 * y0 = 1. R2 ) by A13, Th107, GCD_1:def 2;
consider w0 being object such that
A17: ( w0 in dom phi & z0 = phi . w0 ) by A14, FUNCT_1:def 3;
reconsider w0 = w0 as Element of R1 by A17;
phi . (w0 * x0) = 1. R2 by A1, A15, A16, A17, GROUP_6:def 6;
then A18: w0 * x0 = 1. R1 by A1, Th11;
phi . (x0 * w0) = 1. R2 by A1, A15, A16, A17, GROUP_6:def 6;
then x0 * w0 = 1. R1 by A1, Th11;
then A19: x0 is unital by A18, GCD_1:def 2;
take x0 ; :: thesis: ( x0 in the carrier of (UnitGroup R1) & y = psi . x0 )
A20: x0 in units R1 by A19;
hence x0 in the carrier of (UnitGroup R1) ; :: thesis: y = psi . x0
thus y = psi . x0 by A15, A20, A7; :: thesis: verum

end;

then rng psi = the carrier of (UnitGroup R2) by FUNCT_2:10;
then psi is onto by FUNCT_2:def 3;
hence UnitGroup R1, UnitGroup R2 are_isomorphic by A9, GROUP_6:def 11; :: thesis: verum