:: deftheorem Def12 defines Q*Form HERMITAN:def 12 :
for V, W being VectSp of F_Complex
for f being sesquilinear-Form of V,W
for b₄ being sesquilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer (f *')))) holds
( b₄ = Q*Form 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) );