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 Th69
.= {(0. (VectQuot V,(LKer f)))} by BILINEAR:def 24 ;
rightker (ScalarForm f) = rightker (Q*Form f) by Th59
.= {(0. (VectQuot V,(RKer (f *' ))))} by BILINEAR:def 25
.= {(0. (VectQuot V,(LKer f)))} by Th59 ;
hence A2: ( not ScalarForm f is degenerated-on-left & not ScalarForm f is degenerated-on-right ) by A1, BILINEAR:def 24, BILINEAR:def 25; :: 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, Th61;
hence 0 < Re ((ScalarForm f) . A,A) by Def7; :: thesis: verum