:: deftheorem Def12 defines QFunctional VECTSP10:def 12 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for f being additive Functional of V st the carrier of W c= ker f holds
for b₅ being additive Functional of (VectQuot (V,W)) holds
( b₅ = QFunctional (f,W) iff for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b₅ . A = f . a );