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 additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed
let V, W be non empty ModuleStr over 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 :: thesis: for w being Vector of W holds f . ((v + u),w) = 0. K

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, Th26
.= (0. K) + (f . (u1,w)) by A6
.= (0. K) + (0. K) by A4
.= 0. K by RLVECT_1:def 4 ; :: 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 :: thesis: for w being Vector of W holds f . ((a * v),w) = 0. K

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

end;

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