theorem :: IDEAL_1:78

for R being non empty left_add-cancelable right_zeroed left-distributive left_zeroed doubleLoopStr
for I being non empty Subset of R holds {(0. R)} *' I = {(0. R)}