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 g c= rightker (FormFunctional (f,g))