:: deftheorem Def12 defines QFunctional VECTSP12:def 1 :
for K being Ring
for V, U being VectSp of K
for W being Subspace of V
for f being linear-transformation of V,U st the carrier of W c= the carrier of (ker f) holds
for b₆ being linear-transformation of (VectQuot (V,W)),U 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 );