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