for R being non empty right_add-cancelable right-distributive associative commutative left_zeroed doubleLoopStr
for I being non empty add-closed right-ideal Subset of R
for J, K being Subset of R holds (I % J) % K = I % (J *' K)