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