let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for V, W being non empty VectSpStr of K
for f being additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed
let V, W be non empty VectSpStr of K; :: thesis: for f being additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed
let f be additiveSAF homogeneousSAF Form of V,W; :: thesis: leftker f is linearly-closed
set V1 = leftker f;
thus for v, u being Vector of V st v in leftker f & u in leftker f holds
v + u in leftker 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 V holds
( not b₂ in leftker f or b₁ * b₂ in leftker f )

proof

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

now

let w be Vector of W; :: thesis: f . (v + u),w = 0. K
thus f . (v + u),w = (f . v1,w) + (f . u1,w) by A2, A3, Th27
.= (0. K) + (f . u1,w) by A2
.= (0. K) + (0. K) by A3
.= 0. K by RLVECT_1:def 7 ; :: thesis: verum

end;

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

end;

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

now

let w be Vector of W; :: thesis: f . (a * v),w = 0. K
thus f . (a * v),w = a * (f . v1,w) by A4, Th32
.= a * (0. K) by A4
.= 0. K by VECTSP_1:36 ; :: thesis: verum

end;

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