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 )
assume x in P .: (F -Ideal ) ; :: thesis: x in (P .: F) -Ideal
then consider x' being set such that
A2: ( x' in the carrier of R & x' in F -Ideal & x = P . x' ) by FUNCT_2:115;
consider lc' being LinearCombination of F such that
A3: x' = Sum lc' by A2, IDEAL_1:60;
consider E being FinSequence of [:the carrier of R,the carrier of R,the carrier of R:] such that
A4: E represents lc' by IDEAL_1:35;
consider lc being LinearCombination of P .: F such that
A5: ( len lc' = 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 A4, IDEAL_1:36;
P is RingMonomorphism by A1, QUOFIELD:def 24;
then P is RingHomomorphism by QUOFIELD:def 23;
then x = Sum lc by A2, A3, A4, A5, Th24;
hence x in (P .: F) -Ideal by IDEAL_1:60; :: thesis: verum

end;

then A6: 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 A7: x in (P .: F) -Ideal ; :: thesis: x in P .: (F -Ideal )
then consider lc being LinearCombination of P .: F such that
A8: x = Sum lc by IDEAL_1:60;
( P is RingMonomorphism & P is RingEpimorphism ) by A1, QUOFIELD:def 24;
then A9: ( P is one-to-one & rng P = the carrier of S ) by QUOFIELD:def 22, QUOFIELD:def 23;
then (P " ) .: (P .: F) = P " (P .: F) by FUNCT_1:155;
then A10: (P " ) .: (P .: F) c= F by A9, FUNCT_1:152;
A11: P " = P " by A9, TOPS_2:def 4;
A12: P " is RingIsomorphism by A1, Th25;
consider E being FinSequence of [:the carrier of S,the carrier of S,the carrier of S:] such that
A13: E represents lc by IDEAL_1:35;
consider lc' being LinearCombination of F such that
A14: ( len lc = 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 A10, A11, A13, IDEAL_1:36;
P " is RingMonomorphism by A12, QUOFIELD:def 24;
then P " is RingHomomorphism by QUOFIELD:def 23;
then (P " ) . x = Sum lc' by A8, A13, A14, Th24;
then A15: (P " ) . x in F -Ideal by IDEAL_1:60;
dom P = the carrier of R by FUNCT_2:def 1;
then P . ((P " ) . x) in P .: (F -Ideal ) by A15, FUNCT_1:def 12;
hence x in P .: (F -Ideal ) by A7, A9, A11, FUNCT_1:57; :: thesis: verum

end;

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