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