theorem Th80: :: IDEAL_1:80

for R being non empty add-cancelable Abelian add-associative right_zeroed distributive associative left_zeroed doubleLoopStr
for I, J, K being non empty right-ideal Subset of R holds I *' (J + K) = (I *' J) + (I *' K)