for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a being Element of R holds 1 '*' a = a