let F be non empty right_complementable add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F
for f being linear-Functional of V holds ker f is linearly-closed
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F; :: thesis: for f being linear-Functional of V holds ker f is linearly-closed
let f be linear-Functional of V; :: thesis: ker f is linearly-closed
set V1 = ker f;
thus for v, u being Vector of V st v in ker f & u in ker f holds
v + u in ker f :: according to VECTSP_4:def 1 :: thesis: for b₁ being Element of the carrier of F
for b₂ being Element of the carrier of V holds
( not b₂ in ker f or b₁ * b₂ in ker f )

proof

let v, u be Vector of V; :: thesis: ( v in ker f & u in ker f implies v + u in ker f )
assume ( v in ker f & u in ker f ) ; :: thesis: v + u in ker f
then ( ex a being Vector of V st
( a = v & f . a = 0. F ) & ex b being Vector of V st
( b = u & f . b = 0. F ) ) ;
then f . (v + u) = (0. F) + (0. F) by VECTSP_1:def 20
.= 0. F by RLVECT_1:4 ;
hence v + u in ker f ; :: thesis: verum

end;

let a be Element of F; :: thesis: for b₁ being Element of the carrier of V holds
( not b₁ in ker f or a * b₁ in ker f )
let v be Vector of V; :: thesis: ( not v in ker f or a * v in ker f )
assume v in ker f ; :: thesis: a * v in ker f
then ex w being Vector of V st
( w = v & f . w = 0. F ) ;
then f . (a * v) = a * (0. F) by HAHNBAN1:def 8
.= 0. F ;
hence a * v in ker f ; :: thesis: verum