for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V being non empty ModuleStr over K
for f being symmetric bilinear-Form of V,V holds leftker f = rightker f