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 that
A1: v in leftker f and
A2: u in leftker f ; :: thesis: v + u in leftker f
consider u1 being Vector of V such that
A3: u1 = u and
A4: for w being Vector of W holds f . u1,w = 0. K by A2;
consider v1 being Vector of V such that
A5: v1 = v and
A6: for w being Vector of W holds f . v1,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 A5, A3, Th27
.= (0. K) + (f . u1,w) by A6
.= (0. K) + (0. K) by A4
.= 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
A7: v1 = v and
A8: 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 A7, Th32
.= a * (0. K) by A8
.= 0. K by VECTSP_1:36 ; :: thesis: verum

end;

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