theorem Th4: :: REALSET2:4

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