theorem Th47: :: BILINEAR:47
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V, W being VectSp of K
for f being bilinear-Form of V,W holds LKer f = LKer (RQForm f)