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:
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
.= (P ") . (P . (1_ R)) by
.= 1_ R by ;
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 ;
reconsider x9 = x9 as Element of R by A8;
A10: x9 = (P ") . (P . x9) by
.= (P ") . x by ;
consider y9 being object such that
A11: y9 in the carrier of R and
A12: P . y9 = y by ;
reconsider y9 = y9 as Element of R by A11;
A13: y9 = (P ") . (P . y9) by
.= (P ") . y by ;
A14: (P ") . (x * y) = (P ") . (P . (x9 * y9)) by A5, A9, A12
.= (P ") . (P . (x9 * y9)) by
.= ((P ") . x) * ((P ") . y) by ;
(P ") . (x + y) = (P ") . (P . (x9 + y9)) by A5, A9, A12
.= (P ") . (P . (x9 + y9)) by
.= ((P ") . x) + ((P ") . y) by ;
hence ( (P ") . (x + y) = ((P ") . x) + ((P ") . y) & (P ") . (x * y) = ((P ") . x) * ((P ") . y) & (P ") . (1_ S) = 1_ R ) by ; :: 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 ;
then P " is onto ;
then A17: P " is RingEpimorphism by A15;
P " is one-to-one by ;
hence P " is RingIsomorphism by A17; :: thesis: verum