theorem Th51: :: BILINEAR:51

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 g <> 0Functional W holds
leftker (FormFunctional (f,g)) = ker f