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 ;
A1: ( C = 0 ^2 implies B ^2 <= A * C ) by Th44;
A2: ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * (f . (w,v1))) = |.(f . (w,v1)).| & Im (a * (f . (w,v1))) = 0 ) by Th8;
A3: ( 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:74
.= (A - (((B ^2) * 2) / C)) + (C * ((B / C) ^2))
.= (A - (2 * ((B ^2) / C))) + (C * ((B / C) ^2)) by XCMPLX_1:74
.= (A - (2 * ((B ^2) / C))) + (C * ((B ^2) / (C * C))) by XCMPLX_1:76
.= (A - (2 * ((B ^2) / C))) + ((C * (B ^2)) / (C * C)) by XCMPLX_1:74
.= (A - (2 * ((B ^2) / C))) + ((B ^2) / C) by A4, XCMPLX_1:91
.= A - ((B ^2) / C)
.= ((A * C) - (B ^2)) / C by A4, XCMPLX_1:127 ;
then 0 <= (A * C) - (B ^2) by A2, A4, Th43;
then 0 + (B ^2) <= ((A * C) - (B ^2)) + (B ^2) by XREAL_1:6;
hence B ^2 <= A * C ; :: thesis: verum

end;

B = |.((f . (v1,w)) *').| by Def5
.= |.(f . (v1,w)).| by COMPLEX1:53 ;
hence |.(f . (v1,w)).| ^2 <= (signnorm (f,v1)) * (signnorm (f,w)) by A1, A3, Def7; :: thesis: verum