:: deftheorem defines CQFunctional VECTSP12:def 2 :
for K being Ring
for V, U being VectSp of K
for f being linear-transformation of V,U holds CQFunctional f = QFunctional (f,(ker f));