let R, S be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for F being non empty Subset of R
for P being Function of R,S st P is RingIsomorphism holds
P .: (F -Ideal) = (P .: F) -Ideal
let F be non empty Subset of R; :: thesis: for P being Function of R,S st P is RingIsomorphism holds
P .: (F -Ideal) = (P .: F) -Ideal
let P be Function of R,S; :: thesis: ( P is RingIsomorphism implies P .: (F -Ideal) = (P .: F) -Ideal )
assume A1: P is RingIsomorphism ; :: thesis: P .: (F -Ideal) = (P .: F) -Ideal

now :: thesis: for x being object st x in (P .: F) -Ideal holds
x in P .: (F -Ideal)

let x be object ; :: thesis: ( x in (P .: F) -Ideal implies x in P .: (F -Ideal) )
A2: dom P = the carrier of R by FUNCT_2:def 1;
assume A3: x in (P .: F) -Ideal ; :: thesis: x in P .: (F -Ideal)
then consider lc being LinearCombination of P .: F such that
A4: x = Sum lc by IDEAL_1:60;
consider E being FinSequence of [: the carrier of S, the carrier of S, the carrier of S:] such that
A5: E represents lc by IDEAL_1:35;
P is RingMonomorphism by A1;
then A6: P is one-to-one ;
A7: P is onto by A1;
then A8: P " = P " by A6, TOPS_2:def 4;
(P ") .: (P .: F) = P " (P .: F) by A6, FUNCT_1:85;
then consider lc9 being LinearCombination of F such that
A9: ( len lc = len lc9 & ( for i being set st i in dom lc9 holds
lc9 . i = (((P ") . ((E /. i) `1_3)) * ((P ") . ((E /. i) `2_3))) * ((P ") . ((E /. i) `3_3)) ) ) by A6, A8, A5, FUNCT_1:82, IDEAL_1:36;
P " is RingIsomorphism by A1, Th25;
then P " is RingMonomorphism ;
then P " is RingHomomorphism ;
then (P ") . x = Sum lc9 by A4, A5, A9, Th24;
then (P ") . x in F -Ideal by IDEAL_1:60;
then P . ((P ") . x) in P .: (F -Ideal) by A2, FUNCT_1:def 6;
hence x in P .: (F -Ideal) by A3, A6, A7, A8, FUNCT_1:35; :: thesis: verum

end;

then A10: (P .: F) -Ideal c= P .: (F -Ideal) ;

now :: thesis: for x being object st x in P .: (F -Ideal) holds
x in (P .: F) -Ideal

let x be object ; :: thesis: ( x in P .: (F -Ideal) implies x in (P .: F) -Ideal )
assume x in P .: (F -Ideal) ; :: thesis: x in (P .: F) -Ideal
then consider x9 being object such that
x9 in the carrier of R and
A11: x9 in F -Ideal and
A12: x = P . x9 by FUNCT_2:64;
consider lc9 being LinearCombination of F such that
A13: x9 = Sum lc9 by A11, IDEAL_1:60;
consider E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] such that
A14: E represents lc9 by IDEAL_1:35;
consider lc being LinearCombination of P .: F such that
A15: ( len lc9 = len lc & ( for i being set st i in dom lc holds
lc . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) ) by A14, IDEAL_1:36;
P is RingMonomorphism by A1;
then P is RingHomomorphism ;
then x = Sum lc by A12, A13, A14, A15, Th24;
hence x in (P .: F) -Ideal by IDEAL_1:60; :: thesis: verum

end;

then P .: (F -Ideal) c= (P .: F) -Ideal ;
hence P .: (F -Ideal) = (P .: F) -Ideal by A10, XBOOLE_0:def 10; :: thesis: verum