let V be VectSp of F_Complex ; :: thesis: for v, w being Vector of V
for f being diagReR+0valued hermitan-Form of V holds |.(f . v,w).| ^2 <= (signnorm f,v) * (signnorm f,w)
let v1, w be Vector of V; :: thesis: for f being diagReR+0valued hermitan-Form of V holds |.(f . v1,w).| ^2 <= (signnorm f,v1) * (signnorm f,w)
let f be diagReR+0valued hermitan-Form of V; :: thesis: |.(f . v1,w).| ^2 <= (signnorm f,v1) * (signnorm f,w)
set v4 = f . v1,w;
set w1 = f . w,v1;
set A = signnorm f,v1;
set B = |.(f . w,v1).|;
set C = signnorm f,w;
reconsider A = signnorm f,v1, B = |.(f . w,v1).|, C = signnorm f,w as Real ;
consider a being Element of F_Complex such that
A1: ( |.a.| = 1 & Re (a * (f . w,v1)) = |.(f . w,v1).| & Im (a * (f . w,v1)) = 0 ) by Th9;
A2: B = |.((f . v1,w) *' ).| by Def5
.= |.(f . v1,w).| by COMPLEX1:139 ;
A3: ( C = 0 ^2 implies B ^2 <= A * C ) by Th47;
( C > 0 implies B ^2 <= A * C )

proof

assume A4: C > 0 ; :: thesis: B ^2 <= A * C
(A - ((2 * B) * (B / C))) + (C * ((B / C) ^2 )) = (A - ((B * (2 * B)) / C)) + (C * ((B / C) ^2 )) by XCMPLX_1:75
.= (A - (((B ^2 ) * 2) / C)) + (C * ((B / C) ^2 ))
.= (A - (2 * ((B ^2 ) / C))) + (C * ((B / C) ^2 )) by XCMPLX_1:75
.= (A - (2 * ((B ^2 ) / C))) + (C * ((B ^2 ) / (C * C))) by XCMPLX_1:77
.= (A - (2 * ((B ^2 ) / C))) + ((C * (B ^2 )) / (C * C)) by XCMPLX_1:75
.= (A - (2 * ((B ^2 ) / C))) + ((B ^2 ) / C) by A4, XCMPLX_1:92
.= A - ((B ^2 ) / C)
.= ((A * C) - (B ^2 )) / C by A4, XCMPLX_1:128 ;
then 0 <= ((A * C) - (B ^2 )) / C by A1, Th46;
then 0 <= C * (((A * C) - (B ^2 )) / C) by A4;
then 0 <= (C * ((A * C) - (B ^2 ))) / C by XCMPLX_1:75;
then 0 <= (A * C) - (B ^2 ) by A4;
then 0 + (B ^2 ) <= ((A * C) - (B ^2 )) + (B ^2 ) by XREAL_1:8;
hence B ^2 <= A * C ; :: thesis: verum

end;

hence |.(f . v1,w).| ^2 <= (signnorm f,v1) * (signnorm f,w) by A2, A3, Def7; :: thesis: verum