for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a, b being Element of F holds a * b = b * a