:: deftheorem defines mult| IDEAL_1:def 6 :
for R being non empty multMagma
for I being non empty right-ideal Subset of R holds mult| (I,R) = the multF of R || I;