:: deftheorem defines CQFunctional VECTSP10:def 13 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being VectSp of K
for f being linear-Functional of V holds CQFunctional f = QFunctional (f,(Ker f));