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 } ;

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

suppose not f is degenerated-on-left ; :: thesis: v = 0. V

then {(0. V)} = diagker f by Th52;
hence v = 0. V by A3, TARSKI:def 1; :: thesis: verum

end;

suppose not f is degenerated-on-right ; :: thesis: v = 0. V

then {(0. V)} = diagker f by Th53;
hence v = 0. V by A3, TARSKI:def 1; :: thesis: verum

end;

end;