:: deftheorem defines ScalarForm HERMITAN:def 14 :
for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V holds ScalarForm f = Q*Form f;