theorem Th21: :: REALSET2:21

for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr
for a being Element of F holds
( a * (1. F) = a & (1. F) * a = a )