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

for v being Vector of V st Re (f . (v,v)) = 0 & ( not f is degenerated-on-left or not f is degenerated-on-right ) holds

v = 0. V

let f be diagReR+0valued hermitan-Form of V; :: thesis: for v being Vector of V st Re (f . (v,v)) = 0 & ( not f is degenerated-on-left or not f is degenerated-on-right ) holds

v = 0. V

let v be Vector of V; :: thesis: ( Re (f . (v,v)) = 0 & ( not f is degenerated-on-left or not f is degenerated-on-right ) implies v = 0. V )

assume that

A1: Re (f . (v,v)) = 0 and

A2: ( not f is degenerated-on-left or not f is degenerated-on-right ) ; :: thesis: v = 0. V

f . (v,v) = 0. F_Complex by A1, Th57;

then A3: v in { w where w is Vector of V : f . (w,w) = 0. F_Complex } ;

for v being Vector of V st Re (f . (v,v)) = 0 & ( not f is degenerated-on-left or not f is degenerated-on-right ) holds

v = 0. V

let f be diagReR+0valued hermitan-Form of V; :: thesis: for v being Vector of V st Re (f . (v,v)) = 0 & ( not f is degenerated-on-left or not f is degenerated-on-right ) holds

v = 0. V

let v be Vector of V; :: thesis: ( Re (f . (v,v)) = 0 & ( not f is degenerated-on-left or not f is degenerated-on-right ) implies v = 0. V )

assume that

A1: Re (f . (v,v)) = 0 and

A2: ( not f is degenerated-on-left or not f is degenerated-on-right ) ; :: thesis: v = 0. V

f . (v,v) = 0. F_Complex by A1, Th57;

then A3: v in { w where w is Vector of V : f . (w,w) = 0. F_Complex } ;

per cases
( not f is degenerated-on-left or not f is degenerated-on-right )
by A2;

end;