:: deftheorem Def26 defines alternating BILINEAR:def 26 :
for K being ZeroStr
for V being ModuleStr over K
for f being Form of V,V holds
( f is alternating iff for v being Vector of V holds f . (v,v) = 0. K );