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),(v + w))).| <= ((sqrt |.(f . (v,v)).|) + (sqrt |.(f . (w,w)).|)) ^2
let f be diagReR+0valued hermitan-Form of V; :: thesis: for v, w being Vector of V holds |.(f . ((v + w),(v + w))).| <= ((sqrt |.(f . (v,v)).|) + (sqrt |.(f . (w,w)).|)) ^2
let v1, w be Vector of V; :: thesis: |.(f . ((v1 + w),(v1 + w))).| <= ((sqrt |.(f . (v1,v1)).|) + (sqrt |.(f . (w,w)).|)) ^2
set v3 = f . (v1,v1);
set v4 = f . ((v1 + w),(v1 + w));
set s1 = signnorm (f,v1);
set s2 = signnorm (f,w);
set s12 = signnorm (f,(v1 + w));
A1: |.(f . ((v1 + w),(v1 + w))).| = signnorm (f,(v1 + w)) by Th41;
( signnorm (f,(v1 + w)) <= ((sqrt (signnorm (f,v1))) + (sqrt (signnorm (f,w)))) ^2 & |.(f . (v1,v1)).| = signnorm (f,v1) ) by Th41, Th47;
hence |.(f . ((v1 + w),(v1 + w))).| <= ((sqrt |.(f . (v1,v1)).|) + (sqrt |.(f . (w,w)).|)) ^2 by A1, Th41; :: thesis: verum