let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr of F_Complex ; :: thesis: 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; :: thesis: 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; :: thesis: ( |.(f . v,v).| = Re (f . v,v) & signnorm f,v = |.(f . v,v).| )
set v1 = f . v,v;
set s = signnorm f,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 Th17; :: thesis: verum