theorem :: BILINEAR:59

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 alternating bilinear-Form of V,V holds leftker f = rightker f