theorem Th55: :: BILINEAR:55

for K being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for V being non empty ModuleStr over K
for W being VectSp of K
for f being Functional of V
for g being linear-Functional of W st f <> 0Functional V holds
( RKer (FormFunctional (f,g)) = Ker g & RQForm (FormFunctional (f,g)) = FormFunctional (f,(CQFunctional g)) )