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 linear-Functional of V st the carrier of W c= ker f holds
QFunctional (f,W) is homogeneous