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 )
assume A1: P is RingIsomorphism ; :: thesis: P .: I is Ideal of S
set Q = P .: I;

A2: now

let x, y be Element of S; :: thesis: ( x in P .: I & y in P .: I implies x + y in P .: I )
assume A3: ( x in P .: I & y in P .: I ) ; :: thesis: x + y in P .: I
then consider x' being set such that
A4: ( x' in the carrier of R & x' in I & x = P . x' ) by FUNCT_2:115;
consider y' being set such that
A5: ( y' in the carrier of R & y' in I & y = P . y' ) by A3, FUNCT_2:115;
reconsider x' = x', y' = y' as Element of R by A4, A5;
A6: x' + y' in I by A4, A5, IDEAL_1:def 1;
( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def 24;
then P is RingHomomorphism by QUOFIELD:def 22;
then P is additive by QUOFIELD:def 21;
then x + y = P . (x' + y') by A4, A5, GRCAT_1:def 13;
hence x + y in P .: I by A6, FUNCT_2:43; :: thesis: verum

end;

A7: now

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 x' being set such that
A8: ( x' in the carrier of R & x' in I & x = P . x' ) by FUNCT_2:115;
reconsider x' = x' as Element of R by A8;
A9: ( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def 24;
then rng P = the carrier of S by QUOFIELD:def 22;
then consider p' being set such that
A10: ( p' in dom P & p = P . p' ) by FUNCT_1:def 5;
reconsider p' = p' as Element of R by A10;
A11: p' * x' in I by A8, IDEAL_1:def 2;
P is RingHomomorphism by A9, QUOFIELD:def 22;
then P is multiplicative by QUOFIELD:def 21;
then p * x = P . (p' * x') by A8, A10, GROUP_6:def 7;
hence p * x in P .: I by A11, FUNCT_2:43; :: thesis: verum

end;

now

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 x' being set such that
A12: ( x' in the carrier of R & x' in I & x = P . x' ) by FUNCT_2:115;
reconsider x' = x' as Element of R by A12;
A13: ( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def 24;
then rng P = the carrier of S by QUOFIELD:def 22;
then consider p' being set such that
A14: ( p' in dom P & p = P . p' ) by FUNCT_1:def 5;
reconsider p' = p' as Element of R by A14;
A15: x' * p' in I by A12, IDEAL_1:def 3;
P is RingHomomorphism by A13, QUOFIELD:def 22;
then P is multiplicative by QUOFIELD:def 21;
then x * p = P . (x' * p') by A12, A14, GROUP_6:def 7;
hence x * p in P .: I by A15, FUNCT_2:43; :: thesis: verum

end;

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