:: deftheorem defines multClSet TOPZARI1:def 3 :
for A being non degenerated commutative Ring
for J being proper Ideal of A
for f being Element of A holds multClSet (J,f) = { (f |^ i) where i is Nat : verum } ;