for F being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for x being Element of F holds (0. F) * x = 0. F