theorem Th35: :: VECTSP10:35

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
for A being Vector of (VectQuot (V,(Ker f)))
for v being Vector of V st A = v + (Ker f) holds
(CQFunctional f) . A = f . v