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:29;
hence f . v,v = 0. F_Complex by COMPLFLD:9; :: thesis: verum