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 Th44;
( signnorm f,(v1 + w) <= ((sqrt (signnorm f,v1)) + (sqrt (signnorm f,w))) ^2 & |.(f . v1,v1).| = signnorm f,v1 ) by Th44, Th50;
hence |.(f . (v1 + w),(v1 + w)).| <= ((sqrt |.(f . v1,v1).|) + (sqrt |.(f . w,w).|)) ^2 by A1, Th44; :: thesis: verum