let V be VectSp of F_Complex ; :: thesis: for f being diagReR+0valued hermitan-Form of V holds diagker f is linearly-closed
let f be diagReR+0valued hermitan-Form of V; :: thesis: diagker f is linearly-closed
set V1 = diagker f;
thus for v, u being Element of V st v in diagker f & u in diagker f holds
v + u in diagker f :: according to VECTSP_4:def 1 :: thesis: for b₁ being Element of the carrier of F_Complex
for b₂ being Element of the carrier of V holds
( not b₂ in diagker f or b₁ * b₂ in diagker f )

proof

let v, u be Element of V; :: thesis: ( v in diagker f & u in diagker f implies v + u in diagker f )
assume that
A1: v in diagker f and
A2: u in diagker f ; :: thesis: v + u in diagker f
A3: ex b being Vector of V st
( b = u & f . b,b = 0. F_Complex ) by A2;
then |.(f . v,u).| ^2 <= |.(f . v,v).| * 0 by Th49, COMPLFLD:93;
then A4: |.(f . v,u).| = 0 by XREAL_1:65;
then 0 = |.((f . v,u) *' ).| by COMPLEX1:139
.= |.(f . u,v).| by Def5 ;
then A5: f . u,v = 0. F_Complex by COMPLFLD:94;
ex a being Vector of V st
( a = v & f . a,a = 0. F_Complex ) by A1;
then A6: f . (v + u),(v + u) = ((0. F_Complex ) + (f . v,u)) + ((f . u,v) + (0. F_Complex )) by A3, BILINEAR:29
.= (f . v,u) + ((f . u,v) + (0. F_Complex )) by RLVECT_1:10
.= (f . v,u) + (f . u,v) by RLVECT_1:10 ;
f . v,u = 0. F_Complex by A4, COMPLFLD:94;
then f . (v + u),(v + u) = 0. F_Complex by A6, A5, RLVECT_1:10;
hence v + u in diagker f ; :: thesis: verum

end;

let a be Element of F_Complex ; :: thesis: for b₁ being Element of the carrier of V holds
( not b₁ in diagker f or a * b₁ in diagker f )
let v be Element of V; :: thesis: ( not v in diagker f or a * v in diagker f )
assume v in diagker f ; :: thesis: a * v in diagker f
then A7: ex w being Vector of V st
( w = v & f . w,w = 0. F_Complex ) ;
f . (a * v),(a * v) = a * (f . v,(a * v)) by BILINEAR:32
.= a * ((a *' ) * (0. F_Complex )) by A7, Th30
.= a * (0. F_Complex ) by VECTSP_1:36
.= 0. F_Complex by VECTSP_1:36 ;
hence a * v in diagker f ; :: thesis: verum