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 Th41, Th45;
hence |.(f . (v1,w)).| ^2 <= |.(f . (v1,v1)).| * |.(f . (w,w)).| by Th41; :: thesis: verum