set vq = VectQuot (V,(LKer f));

set vr = VectQuot (V,(RKer (f *')));

set qh = ScalarForm f;

A1: leftker (ScalarForm f) = leftker (Q*Form f) by Th66

.= {(0. (VectQuot (V,(LKer f))))} by BILINEAR:def 23 ;

rightker (ScalarForm f) = rightker (Q*Form f) by Th56

.= {(0. (VectQuot (V,(RKer (f *')))))} by BILINEAR:def 24

.= {(0. (VectQuot (V,(LKer f))))} by Th56 ;

hence A2: ( not ScalarForm f is degenerated-on-left & not ScalarForm f is degenerated-on-right ) by A1; :: thesis: ScalarForm f is positivediagvalued

let A be Vector of (VectQuot (V,(LKer f))); :: according to HERMITAN:def 13 :: thesis: ( A <> 0. (VectQuot (V,(LKer f))) implies 0 < Re ((ScalarForm f) . (A,A)) )

assume A <> 0. (VectQuot (V,(LKer f))) ; :: thesis: 0 < Re ((ScalarForm f) . (A,A))

then Re ((ScalarForm f) . (A,A)) <> 0 by A2, Th58;

hence 0 < Re ((ScalarForm f) . (A,A)) by Def7; :: thesis: verum

set vr = VectQuot (V,(RKer (f *')));

set qh = ScalarForm f;

A1: leftker (ScalarForm f) = leftker (Q*Form f) by Th66

.= {(0. (VectQuot (V,(LKer f))))} by BILINEAR:def 23 ;

rightker (ScalarForm f) = rightker (Q*Form f) by Th56

.= {(0. (VectQuot (V,(RKer (f *')))))} by BILINEAR:def 24

.= {(0. (VectQuot (V,(LKer f))))} by Th56 ;

hence A2: ( not ScalarForm f is degenerated-on-left & not ScalarForm f is degenerated-on-right ) by A1; :: thesis: ScalarForm f is positivediagvalued

let A be Vector of (VectQuot (V,(LKer f))); :: according to HERMITAN:def 13 :: thesis: ( A <> 0. (VectQuot (V,(LKer f))) implies 0 < Re ((ScalarForm f) . (A,A)) )

assume A <> 0. (VectQuot (V,(LKer f))) ; :: thesis: 0 < Re ((ScalarForm f) . (A,A))

then Re ((ScalarForm f) . (A,A)) <> 0 by A2, Th58;

hence 0 < Re ((ScalarForm f) . (A,A)) by Def7; :: thesis: verum