:: deftheorem defines constant VECTSP10:def 7 :
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V being non empty right_zeroed ModuleStr over K
for f being 0-preserving Functional of V holds
( f is constant iff f = 0Functional V );