:: deftheorem defines Fanoian VECTSP_1:def 18 :
for F being non empty non degenerated right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr holds
( F is Fanoian iff (1. F) + (1. F) <> 0. F );