:: deftheorem Def2 defines " VECTSP_2:def 2 :
for SF being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative doubleLoopStr
for x being Element of SF st x <> 0. SF holds
for b₃ being Element of the carrier of SF holds
( b₃ = x " iff b₃ * x = 1. SF );