let R, S be non empty doubleLoopStr ; :: thesis: for P being Function of R,S st P is RingIsomorphism holds
P " is RingIsomorphism
let P be Function of R,S; :: thesis: ( P is RingIsomorphism implies P " is RingIsomorphism )
assume A1: P is RingIsomorphism ; :: thesis: P " is RingIsomorphism
then A2: P is RingEpimorphism ;
then A3: P is onto ;
A4: P is one-to-one by A1;
A5: ( P is additive & P is multiplicative & P is unity-preserving ) by A2;
for x, y being Element of S holds
( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R )

proof

A6: P is onto by A3;
A7: (P ") . (1_ S) = (P ") . (P . (1_ R)) by A5, GROUP_1:def 13
.= (P ") . (P . (1_ R)) by A4, A6, TOPS_2:def 4
.= 1_ R by A4, FUNCT_2:26 ;
let x, y be Element of S; :: thesis: ( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R )
consider x9 being object such that
A8: x9 in the carrier of R and
A9: P . x9 = x by A3, FUNCT_2:11;
reconsider x9 = x9 as Element of R by A8;
A10: x9 = (P ") . (P . x9) by A4, FUNCT_2:26
.= (P ") . x by A4, A9, A6, TOPS_2:def 4 ;
consider y9 being object such that
A11: y9 in the carrier of R and
A12: P . y9 = y by A3, FUNCT_2:11;
reconsider y9 = y9 as Element of R by A11;
A13: y9 = (P ") . (P . y9) by A4, FUNCT_2:26
.= (P ") . y by A6, A4, A12, TOPS_2:def 4 ;
A14: (P ") . (x * y) = (P ") . (P . (x9 * y9)) by A5, A9, A12
.= (P ") . (P . (x9 * y9)) by A4, A6, TOPS_2:def 4
.= ((P ") . x) * ((P ") . y) by A4, A10, A13, FUNCT_2:26 ;
(P ") . (x + y) = (P ") . (P . (x9 + y9)) by A5, A9, A12
.= (P ") . (P . (x9 + y9)) by A4, A6, TOPS_2:def 4
.= ((P ") . x) + ((P ") . y) by A4, A10, A13, FUNCT_2:26 ;
hence ( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R ) by A14, A7; :: thesis: verum

end;

then ( P " is additive & P " is multiplicative & P " is unity-preserving ) by GROUP_1:def 13;
then A15: P " is RingHomomorphism ;
A16: rng P = [#] S by A3;
then rng (P ") = [#] R by A4, TOPS_2:49;
then P " is onto ;
then A17: P " is RingEpimorphism by A15;
P " is one-to-one by A4, A16, TOPS_2:50;
hence P " is RingIsomorphism by A17; :: thesis: verum