theorem Th53: :: BILINEAR:53

for K being non empty right_complementable almost_left_invertible add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for V, W being non empty ModuleStr over K
for f being Functional of V
for g being Functional of W st f <> 0Functional V holds
rightker (FormFunctional (f,g)) = ker g