let R, S be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive 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

let x be set ; :: 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, QUOFIELD:def 24;
then A6: P is one-to-one by QUOFIELD:def 23;
P is RingEpimorphism by A1, QUOFIELD:def 24;
then A7: rng P = the carrier of S by QUOFIELD:def 22;
then A8: P " = P " by A6, TOPS_2:def 4;
(P " ) .: (P .: F) = P " (P .: F) by A6, FUNCT_1:155;
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 )) * ((P " ) . ((E /. i) `2 ))) * ((P " ) . ((E /. i) `3 )) ) ) by A6, A8, A5, FUNCT_1:152, IDEAL_1:36;
P " is RingIsomorphism by A1, Th25;
then P " is RingMonomorphism by QUOFIELD:def 24;
then P " is RingHomomorphism by QUOFIELD:def 23;
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 12;
hence x in P .: (F -Ideal ) by A3, A6, A7, A8, FUNCT_1:57; :: thesis: verum

end;

then A10: (P .: F) -Ideal c= P .: (F -Ideal ) by TARSKI:def 3;

now

let x be set ; :: 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 set such that
x9 in the carrier of R and
A11: x9 in F -Ideal and
A12: x = P . x9 by FUNCT_2:115;
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 )) * (P . ((E /. i) `2 ))) * (P . ((E /. i) `3 )) ) ) by A14, IDEAL_1:36;
P is RingMonomorphism by A1, QUOFIELD:def 24;
then P is RingHomomorphism by QUOFIELD:def 23;
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 by TARSKI:def 3;
hence P .: (F -Ideal ) = (P .: F) -Ideal by A10, XBOOLE_0:def 10; :: thesis: verum