let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for V, W being non empty ModuleStr over K
for f being additiveFAF homogeneousFAF Form of V,W holds rightker f is linearly-closed
let V, W be non empty ModuleStr over K; :: thesis: for f being additiveFAF homogeneousFAF Form of V,W holds rightker f is linearly-closed
let f be additiveFAF homogeneousFAF Form of V,W; :: thesis: rightker f is linearly-closed
set V1 = rightker f;
thus for v, u being Vector of W st v in rightker f & u in rightker f holds
v + u in rightker f :: according to VECTSP_4:def 1 :: thesis: for b₁ being Element of the carrier of K
for b₂ being Element of the carrier of W holds
( not b₂ in rightker f or b₁ * b₂ in rightker f )

proof

let v, u be Vector of W; :: thesis: ( v in rightker f & u in rightker f implies v + u in rightker f )
assume that
A1: v in rightker f and
A2: u in rightker f ; :: thesis: v + u in rightker f
consider u1 being Vector of W such that
A3: u1 = u and
A4: for w being Vector of V holds f . (w,u1) = 0. K by A2;
consider v1 being Vector of W such that
A5: v1 = v and
A6: for w being Vector of V holds f . (w,v1) = 0. K by A1;

now :: thesis: for w being Vector of V holds f . (w,(v + u)) = 0. K

let w be Vector of V; :: thesis: f . (w,(v + u)) = 0. K
thus f . (w,(v + u)) = (f . (w,v1)) + (f . (w,u1)) by A5, A3, Th27
.= (0. K) + (f . (w,u1)) by A6
.= (0. K) + (0. K) by A4
.= 0. K by RLVECT_1:def 4 ; :: thesis: verum

end;

hence v + u in rightker f ; :: thesis: verum

end;

let a be Element of K; :: thesis: for b₁ being Element of the carrier of W holds
( not b₁ in rightker f or a * b₁ in rightker f )
let v be Vector of W; :: thesis: ( not v in rightker f or a * v in rightker f )
assume v in rightker f ; :: thesis: a * v in rightker f
then consider v1 being Vector of W such that
A7: v1 = v and
A8: for w being Vector of V holds f . (w,v1) = 0. K ;

now :: thesis: for w being Vector of V holds f . (w,(a * v)) = 0. K

let w be Vector of V; :: thesis: f . (w,(a * v)) = 0. K
thus f . (w,(a * v)) = a * (f . (w,v1)) by A7, Th32
.= a * (0. K) by A8
.= 0. K ; :: thesis: verum

end;

hence a * v in rightker f ; :: thesis: verum