let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F_Complex ; for f being diagRvalued diagReR+0valued Form of V,V
for v being Vector of V holds
( |.(f . (v,v)).| = Re (f . (v,v)) & signnorm (f,v) = |.(f . (v,v)).| )
let f be diagRvalued diagReR+0valued Form of V,V; for v being Vector of V holds
( |.(f . (v,v)).| = Re (f . (v,v)) & signnorm (f,v) = |.(f . (v,v)).| )
let v be Vector of V; ( |.(f . (v,v)).| = Re (f . (v,v)) & signnorm (f,v) = |.(f . (v,v)).| )
set v1 = f . (v,v);
( 0 <= Re (f . (v,v)) & Im (f . (v,v)) = 0 )
by Def6, Def7;
hence
( |.(f . (v,v)).| = Re (f . (v,v)) & signnorm (f,v) = |.(f . (v,v)).| )
by Th14; verum