:: deftheorem Def16 defines scalar-unital VECTSP_1:def 16 :
for F being non empty doubleLoopStr
for IT being non empty ModuleStr over F holds
( IT is scalar-unital iff for v being Element of IT holds (1. F) * v = v );