let R, S be non empty doubleLoopStr ; :: thesis: ( ex f being Function of R,S st f is RingIsomorphism implies ex f being Function of S,R st f is RingIsomorphism )
given f being Function of R,S such that A1: f is RingIsomorphism ; :: thesis: ex f being Function of S,R st f is RingIsomorphism
A2: f is onto by A1;
then A3: rng f = [#] S ;
set g = f " ;
A4: f is one-to-one by A1;
A5: f is RingHomomorphism by A1;
for x, y being Element of S holds
( (f ") . (x + y) = ((f ") . x) + ((f ") . y) & (f ") . (x * y) = ((f ") . x) * ((f ") . y) & (f ") . (1_ S) = 1_ R )

proof

let x, y be Element of S; :: thesis: ( (f ") . (x + y) = ((f ") . x) + ((f ") . y) & (f ") . (x * y) = ((f ") . x) * ((f ") . y) & (f ") . (1_ S) = 1_ R )
consider x9 being object such that
A6: x9 in the carrier of R and
A7: f . x9 = x by A3, FUNCT_2:11;
reconsider x9 = x9 as Element of R by A6;
A8: x9 = (f ") . (f . x9) by A4, FUNCT_2:26
.= (f ") . x by A4, A7, A2, TOPS_2:def 4 ;
consider y9 being object such that
A9: y9 in the carrier of R and
A10: f . y9 = y by A3, FUNCT_2:11;
reconsider y9 = y9 as Element of R by A9;
A11: y9 = (f ") . (f . y9) by A4, FUNCT_2:26
.= (f ") . y by A4, A10, A2, TOPS_2:def 4 ;
thus (f ") . (x + y) = (f ") . (f . (x9 + y9)) by A5, A7, A10, VECTSP_1:def 20
.= (f ") . (f . (x9 + y9)) by A2, A4, TOPS_2:def 4
.= ((f ") . x) + ((f ") . y) by A4, A8, A11, FUNCT_2:26 ; :: thesis: ( (f ") . (x * y) = ((f ") . x) * ((f ") . y) & (f ") . (1_ S) = 1_ R )
thus (f ") . (x * y) = (f ") . (f . (x9 * y9)) by A5, A7, A10, GROUP_6:def 6
.= (f ") . (f . (x9 * y9)) by A2, A4, TOPS_2:def 4
.= ((f ") . x) * ((f ") . y) by A4, A8, A11, FUNCT_2:26 ; :: thesis: (f ") . (1_ S) = 1_ R
thus (f ") . (1_ S) = (f ") . (f . (1_ R)) by A5, GROUP_1:def 13
.= (f ") . (f . (1_ R)) by A2, A4, TOPS_2:def 4
.= 1_ R by A4, FUNCT_2:26 ; :: thesis: verum

end;

then A12: ( f " is additive & f " is multiplicative & f " is unity-preserving ) by GROUP_1:def 13, GROUP_6:def 6;
rng (f ") = [#] R by A3, A4, TOPS_2:49;
then f " is onto ;
then A13: f " is RingEpimorphism by A12;
f " is one-to-one by A3, A4, TOPS_2:50;
then f " is RingMonomorphism by A12;
hence ex f being Function of S,R st f is RingIsomorphism by A13; :: thesis: verum