theorem :: HERMITAN:65

for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for A, B being Vector of (VectQuot (V,(LKer f)))
for v, w being Vector of V st A = v + (LKer f) & B = w + (LKer f) holds
(ScalarForm f) . (A,B) = f . (v,w)