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 Th46, COMPLFLD:57;
then A4: |.(f . (v,u)).| = 0 by XREAL_1:63;
then 0 = |.((f . (v,u)) *').| by COMPLEX1:53
.= |.(f . (u,v)).| by Def5 ;
then A5: f . (u,v) = 0. F_Complex by COMPLFLD:58;
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:28
.= (f . (v,u)) + ((f . (u,v)) + (0. F_Complex)) by RLVECT_1:4
.= (f . (v,u)) + (f . (u,v)) by RLVECT_1:4 ;
f . (v,u) = 0. F_Complex by A4, COMPLFLD:58;
then f . ((v + u),(v + u)) = 0. F_Complex by A6, A5, RLVECT_1:4;
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:31
.= a * ((a *') * (0. F_Complex)) by A7, Th27
.= 0. F_Complex ;
hence a * v in diagker f ; :: thesis: verum