let V be VectSp of F_Complex ; :: thesis: for f being diagReR+0valued hermitan-Form of V
for v, w being Vector of V holds |.(f . v,w).| ^2 <= |.(f . v,v).| * |.(f . w,w).|
let f be diagReR+0valued hermitan-Form of V; :: thesis: for v, w being Vector of V holds |.(f . v,w).| ^2 <= |.(f . v,v).| * |.(f . w,w).|
let v1, w be Vector of V; :: thesis: |.(f . v1,w).| ^2 <= |.(f . v1,v1).| * |.(f . w,w).|
set v3 = f . v1,v1;
set s1 = signnorm f,v1;
set s2 = signnorm f,w;
( |.(f . v1,w).| ^2 <= (signnorm f,v1) * (signnorm f,w) & signnorm f,v1 = |.(f . v1,v1).| ) by Th44, Th48;
hence |.(f . v1,w).| ^2 <= |.(f . v1,v1).| * |.(f . w,w).| by Th44; :: thesis: verum