set F = the strict Field;
( the strict Field is unital & the strict Field is distributive ) ;
hence ex b₁ being non empty doubleLoopStr st
( b₁ is strict & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is unital & b₁ is distributive ) ; :: thesis: verum