let R, S be non empty doubleLoopStr ; :: thesis: for I being Ideal of R
for P being Function of R,S st P is RingIsomorphism holds
P .: I is Ideal of S
let I be Ideal of R; :: thesis: for P being Function of R,S st P is RingIsomorphism holds
P .: I is Ideal of S
let P be Function of R,S; :: thesis: ( P is RingIsomorphism implies P .: I is Ideal of S )
set Q = P .: I;
assume A1: P is RingIsomorphism ; :: thesis: P .: I is Ideal of S

A2: now :: thesis: for p, x being Element of S st x in P .: I holds
p * x in P .: I

let p, x be Element of S; :: thesis: ( x in P .: I implies p * x in P .: I )
assume x in P .: I ; :: thesis: p * x in P .: I
then consider x9 being object such that
A3: x9 in the carrier of R and
A4: x9 in I and
A5: x = P . x9 by FUNCT_2:64;
reconsider x9 = x9 as Element of R by A3;
A6: ( P is RingMonomorphism & P is RingEpimorphism ) by A1;
then P is onto ;
then consider p9 being object such that
A7: p9 in dom P and
A8: p = P . p9 by FUNCT_1:def 3;
reconsider p9 = p9 as Element of R by A7;
A9: p9 * x9 in I by A4, IDEAL_1:def 2;
P is RingHomomorphism by A6;
then P is multiplicative ;
then p * x = P . (p9 * x9) by A5, A8;
hence p * x in P .: I by A9, FUNCT_2:35; :: thesis: verum

end;

A10: now :: thesis: for p, x being Element of S st x in P .: I holds
x * p in P .: I

let p, x be Element of S; :: thesis: ( x in P .: I implies x * p in P .: I )
assume x in P .: I ; :: thesis: x * p in P .: I
then consider x9 being object such that
A11: x9 in the carrier of R and
A12: x9 in I and
A13: x = P . x9 by FUNCT_2:64;
reconsider x9 = x9 as Element of R by A11;
A14: ( P is RingMonomorphism & P is RingEpimorphism ) by A1;
then P is onto ;
then consider p9 being object such that
A15: p9 in dom P and
A16: p = P . p9 by FUNCT_1:def 3;
reconsider p9 = p9 as Element of R by A15;
A17: x9 * p9 in I by A12, IDEAL_1:def 3;
P is RingHomomorphism by A14;
then P is multiplicative ;
then x * p = P . (x9 * p9) by A13, A16;
hence x * p in P .: I by A17, FUNCT_2:35; :: thesis: verum

end;

now :: thesis: for x, y being Element of S st x in P .: I & y in P .: I holds
x + y in P .: I

let x, y be Element of S; :: thesis: ( x in P .: I & y in P .: I implies x + y in P .: I )
assume that
A18: x in P .: I and
A19: y in P .: I ; :: thesis: x + y in P .: I
consider x9 being object such that
A20: x9 in the carrier of R and
A21: x9 in I and
A22: x = P . x9 by A18, FUNCT_2:64;
consider y9 being object such that
A23: y9 in the carrier of R and
A24: y9 in I and
A25: y = P . y9 by A19, FUNCT_2:64;
reconsider x9 = x9, y9 = y9 as Element of R by A20, A23;
A26: x9 + y9 in I by A21, A24, IDEAL_1:def 1;
( P is RingMonomorphism & P is RingEpimorphism ) by A1;
then P is additive ;
then x + y = P . (x9 + y9) by A22, A25;
hence x + y in P .: I by A26, FUNCT_2:35; :: thesis: verum

end;

hence P .: I is Ideal of S by A2, A10, IDEAL_1:def 1, IDEAL_1:def 2, IDEAL_1:def 3; :: thesis: verum