let V be 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)
let f be 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)
set vq = VectQuot (V,(LKer f));
set vr = VectQuot (V,(RKer (f *')));
let A, B be 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)
let v, w be Vector of V; ( A = v + (LKer f) & B = w + (LKer f) implies (ScalarForm f) . (A,B) = f . (v,w) )
reconsider W = B as Vector of (VectQuot (V,(RKer (f *')))) by Th56;
assume that
A1:
A = v + (LKer f)
and
A2:
B = w + (LKer f)
; (ScalarForm f) . (A,B) = f . (v,w)
W = w + (RKer (f *'))
by A2, Th56;
hence
(ScalarForm f) . (A,B) = f . (v,w)
by A1, Def12; verum