for R being non empty left_unital doubleLoopStr
for I being Subset of R holds (1. R) * I = I