:: deftheorem Def25 defines symmetric BILINEAR:def 25 :
for K being 1-sorted
for V being ModuleStr over K
for f being Form of V,V holds
( f is symmetric iff for v, w being Vector of V holds f . (v,w) = f . (w,v) );