:: deftheorem Def23 defines degenerated-on-left BILINEAR:def 23 :
for K being ZeroStr
for V, W being non empty ModuleStr over K
for f being Form of V,W holds
( f is degenerated-on-left iff leftker f <> {(0. V)} );