theorem Th6: :: REALSET2:6

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