let V be VectSp of F_Complex ; :: thesis: 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; :: thesis: 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))); :: thesis: 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; :: thesis: ( 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) ; :: thesis: (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; :: thesis: verum

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; :: thesis: 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))); :: thesis: 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; :: thesis: ( 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) ; :: thesis: (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; :: thesis: verum