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