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;
consider a being Element of F_Complex such that
A1: ( |.a.| = 1 & Re (a * (f . w,v1)) = |.(f . w,v1).| & Im (a * (f . w,v1)) = 0 ) by Th9;
reconsider A = signnorm f,v1 as Real ;
assume that
A2: signnorm f,w = 0 and
A3: |.(f . w,v1).| <> 0 ; :: thesis: contradiction

A4: now

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

A6: now

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

end;

now

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

end;

hence contradiction by A3, A6; :: thesis: verum

end;

now

assume A10: A <> 0 ; :: thesis: contradiction

A11: now

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

end;

now

assume A13: 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 A2, XCMPLX_1:75
.= A - (((A * 2) * |.(f . w,v1).|) / |.(f . w,v1).|)
.= A - (A + A) by A3, XCMPLX_1:90
.= - A ;
then 0 <= - A by A1, Th46;
then - (- A) <= - 0 ;
hence contradiction by A13; :: thesis: verum

end;

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

end;

hence contradiction by A4; :: thesis: verum