let V be VectSp of F_Complex ; :: thesis: for f being diagRvalued diagReR+0valued Form of V,V

for v being Vector of V st Re (f . (v,v)) = 0 holds

f . (v,v) = 0. F_Complex

let f be diagRvalued diagReR+0valued Form of V,V; :: thesis: for v being Vector of V st Re (f . (v,v)) = 0 holds

f . (v,v) = 0. F_Complex

let v be Vector of V; :: thesis: ( Re (f . (v,v)) = 0 implies f . (v,v) = 0. F_Complex )

assume A1: Re (f . (v,v)) = 0 ; :: thesis: f . (v,v) = 0. F_Complex

Im (f . (v,v)) = 0 by Def6;

then f . (v,v) = 0 + (0 * <i>) by A1, COMPLEX1:13;

hence f . (v,v) = 0. F_Complex by COMPLFLD:7; :: thesis: verum

for v being Vector of V st Re (f . (v,v)) = 0 holds

f . (v,v) = 0. F_Complex

let f be diagRvalued diagReR+0valued Form of V,V; :: thesis: for v being Vector of V st Re (f . (v,v)) = 0 holds

f . (v,v) = 0. F_Complex

let v be Vector of V; :: thesis: ( Re (f . (v,v)) = 0 implies f . (v,v) = 0. F_Complex )

assume A1: Re (f . (v,v)) = 0 ; :: thesis: f . (v,v) = 0. F_Complex

Im (f . (v,v)) = 0 by Def6;

then f . (v,v) = 0 + (0 * <i>) by A1, COMPLEX1:13;

hence f . (v,v) = 0. F_Complex by COMPLFLD:7; :: thesis: verum