:: deftheorem Def22 defines QForm BILINEAR:def 22 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V, W being VectSp of K
for f being bilinear-Form of V,W
for b₅ being bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))) holds
( b₅ = QForm f iff for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
b₅ . (A,B) = f . (v,w) );