:: deftheorem Def10 defines " VECTSP_1:def 10 :
for F being non empty almost_left_invertible associative commutative well-unital doubleLoopStr
for x being Element of F st x <> 0. F holds
for b₃ being Element of the carrier of F holds
( b₃ = x " iff b₃ * x = 1. F );