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 .: () = (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 .: () = (P .: F) -Ideal

let P be Function of R,S; :: thesis: ( P is RingIsomorphism implies P .: () = (P .: F) -Ideal )
assume A1: P is RingIsomorphism ; :: thesis: P .: () = (P .: F) -Ideal
now :: thesis: for x being object st x in (P .: F) -Ideal holds
x in P .: ()
let x be object ; :: thesis: ( x in (P .: F) -Ideal implies x in P .: () )
A2: dom P = the carrier of R by FUNCT_2:def 1;
assume A3: x in (P .: F) -Ideal ; :: thesis: x in P .: ()
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 ;
(P ") .: (P .: F) = P " (P .: F) by ;
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 ;
P " is RingIsomorphism by ;
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 .: () by ;
hence x in P .: () by ; :: thesis: verum
end;
then A10: (P .: F) -Ideal c= P .: () ;
now :: thesis: for x being object st x in P .: () holds
x in (P .: F) -Ideal
let x be object ; :: thesis: ( x in P .: () implies x in (P .: F) -Ideal )
assume x in P .: () ; :: 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 ;
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 ;
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 .: () c= (P .: F) -Ideal ;
hence P .: () = (P .: F) -Ideal by ; :: thesis: verum