:: deftheorem Def20 defines LQForm BILINEAR:def 20 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being VectSp of K
for W being non empty ModuleStr over K
for f being additiveSAF homogeneousSAF Form of V,W
for b₅ being additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W holds
( b₅ = LQForm f iff for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b₅ . (A,w) = f . (v,w) );