theorem Th47: :: HERMITAN:47

for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V
for v, w being Vector of V holds signnorm (f,(v + w)) <= ((sqrt (signnorm (f,v))) + (sqrt (signnorm (f,w)))) ^2