theorem Th50: :: BILINEAR:50

for K being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for V, W being non empty ModuleStr over K
for f being Functional of V
for g being Functional of W holds ker f c= leftker (FormFunctional (f,g))