:: deftheorem Def21 defines RQForm BILINEAR:def 21 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being non empty ModuleStr over K
for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W
for b₅ being additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))) holds
( b₅ = RQForm f iff for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b₅ . (v,A) = f . (v,w) );