:: deftheorem Def4 defines Field-like REALSET2:def 4 :
for L being doubleLoopStr holds
( L is Field-like iff ( the multF of L is the carrier of L \ {(0. L)} -subsetpreserving & ( for B being non empty set
for P being BinOp of B
for e being Element of B st B = NonZero L & e = 1. L & P = the multF of L || (NonZero L) holds
addLoopStr(# B,P,e #) is AbGroup ) ) );