theorem Th54: :: BILINEAR:54

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