let V be VectSp of F_Complex ; :: thesis: for v, w being Vector of V
for f being diagReR+0valued hermitan-Form of V st signnorm f,w = 0 holds
|.(f . w,v).| = 0
let v1, w be Vector of V; :: thesis: for f being diagReR+0valued hermitan-Form of V st signnorm f,w = 0 holds
|.(f . w,v1).| = 0
let f be diagReR+0valued hermitan-Form of V; :: thesis: ( signnorm f,w = 0 implies |.(f . w,v1).| = 0 )
set w1 = f . w,v1;
set A = signnorm f,v1;
set B = |.(f . w,v1).|;
set C = signnorm f,w;
reconsider A = signnorm f,v1 as Real ;
assume that
A1: signnorm f,w = 0 and
A2: |.(f . w,v1).| <> 0 ; :: thesis: contradiction
A3: ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * (f . w,v1)) = |.(f . w,v1).| & Im (a * (f . w,v1)) = 0 ) by Th9;

A4: now

A5: now

assume A6: A > 0 ; :: thesis: contradiction
(A - ((2 * |.(f . w,v1).|) * (A / |.(f . w,v1).|))) + ((signnorm f,w) * ((A / |.(f . w,v1).|) ^2 )) = A - ((A * (2 * |.(f . w,v1).|)) / |.(f . w,v1).|) by A1, XCMPLX_1:75
.= A - (((A * 2) * |.(f . w,v1).|) / |.(f . w,v1).|)
.= A - (A + A) by A2, XCMPLX_1:90
.= - A ;
hence contradiction by A3, A6, Th46; :: thesis: verum

end;

A7: now

assume A8: A < 0 ; :: thesis: contradiction
0 <= (A - ((2 * |.(f . w,v1).|) * 0 )) + ((signnorm f,w) * (0 ^2 )) by A3, Th46;
hence contradiction by A8; :: thesis: verum

end;

assume A <> 0 ; :: thesis: contradiction
hence contradiction by A7, A5; :: thesis: verum

end;

now

assume A9: A = 0 ; :: thesis: contradiction

A10: now

assume A11: 0 < |.(f . w,v1).| ; :: thesis: contradiction
0 <= (A - ((2 * |.(f . w,v1).|) * 1)) + ((signnorm f,w) * (1 ^2 )) by A3, Th46;
hence contradiction by A1, A9, A11; :: thesis: verum

end;

now

assume A12: |.(f . w,v1).| < 0 ; :: thesis: contradiction
0 <= (A - ((2 * |.(f . w,v1).|) * (- 1))) + ((signnorm f,w) * ((- 1) ^2 )) by A3, Th46;
hence contradiction by A1, A9, A12; :: thesis: verum

end;

hence contradiction by A2, A10; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum