set V = (width A) -VectSp_over K;
set k0 = k |-> (0. K);
set S = Solutions_of (A,(k |-> (0. K)));
A1: ColVec2Mx (k |-> (0. K)) = 0. (K,k,1) by Th32;

A2: now :: thesis: for a being Element of K
for v being Element of ((width A) -VectSp_over K) st v in Solutions_of (A,(k |-> (0. K))) holds
a * v in Solutions_of (A,(k |-> (0. K)))

let a be Element of K; :: thesis: for v being Element of ((width A) -VectSp_over K) st v in Solutions_of (A,(k |-> (0. K))) holds
a * v in Solutions_of (A,(k |-> (0. K)))
let v be Element of ((width A) -VectSp_over K); :: thesis: ( v in Solutions_of (A,(k |-> (0. K))) implies a * v in Solutions_of (A,(k |-> (0. K))) )
assume v in Solutions_of (A,(k |-> (0. K))) ; :: thesis: a * v in Solutions_of (A,(k |-> (0. K)))
then consider f being FinSequence of K such that
A3: v = f and
A4: ColVec2Mx f in Solutions_of (A,(ColVec2Mx (k |-> (0. K)))) ;
reconsider f = f as Element of (width A) -tuples_on the carrier of K by A3, MATRIX13:102;

now :: thesis: 0. (K,k,1) = a * (0. (K,k,1))

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: 0. (K,k,1) = a * (0. (K,k,1))

then ( len (a * (0. (K,k,1))) = len (0. (K,k,1)) & 0. (K,k,1) = {} ) by MATRIX_3:def 5;
hence 0. (K,k,1) = a * (0. (K,k,1)) ; :: thesis: verum

end;

suppose A5: k > 0 ; :: thesis: a * (0. (K,k,1)) = 0. (K,k,1)

then A6: ( len (0. (K,k,1)) = k & width (0. (K,k,1)) = 1 ) by MATRIX_0:23;
hence a * (0. (K,k,1)) = a * ((0. K) * (0. (K,k,1))) by A5, MATRIX_5:24
.= (a * (0. K)) * (0. (K,k,1)) by MATRIX_5:11
.= (0. K) * (0. (K,k,1))
.= 0. (K,k,1) by A5, A6, MATRIX_5:24 ;
:: thesis: verum

end;

end;

end;

then a * (ColVec2Mx f) in Solutions_of (A,(0. (K,k,1))) by A1, A4, Th35;
then ColVec2Mx (a * f) in Solutions_of (A,(0. (K,k,1))) by Th30;
then a * f in Solutions_of (A,(k |-> (0. K))) by A1;
hence a * v in Solutions_of (A,(k |-> (0. K))) by A3, MATRIX13:102; :: thesis: verum

end;

now :: thesis: for v, u being Element of ((width A) -VectSp_over K) st v in Solutions_of (A,(k |-> (0. K))) & u in Solutions_of (A,(k |-> (0. K))) holds
v + u in Solutions_of (A,(k |-> (0. K)))

let v, u be Element of ((width A) -VectSp_over K); :: thesis: ( v in Solutions_of (A,(k |-> (0. K))) & u in Solutions_of (A,(k |-> (0. K))) implies v + u in Solutions_of (A,(k |-> (0. K))) )
assume that
A7: v in Solutions_of (A,(k |-> (0. K))) and
A8: u in Solutions_of (A,(k |-> (0. K))) ; :: thesis: v + u in Solutions_of (A,(k |-> (0. K)))
consider f being FinSequence of K such that
A9: v = f and
A10: ColVec2Mx f in Solutions_of (A,(ColVec2Mx (k |-> (0. K)))) by A7;
consider g being FinSequence of K such that
A11: u = g and
A12: ColVec2Mx g in Solutions_of (A,(ColVec2Mx (k |-> (0. K)))) by A8;
A13: len g = width A by A12, Th59;
reconsider f = f, g = g as Element of (width A) -tuples_on the carrier of K by A9, A11, MATRIX13:102;
(ColVec2Mx f) + (ColVec2Mx g) in Solutions_of (A,((0. (K,k,1)) + (0. (K,k,1)))) by A1, A10, A12, Th37;
then (ColVec2Mx f) + (ColVec2Mx g) in Solutions_of (A,(0. (K,k,1))) by MATRIX_3:4;
then ColVec2Mx (f + g) in Solutions_of (A,(0. (K,k,1))) by A10, A13, Th28, Th59;
then f + g in Solutions_of (A,(k |-> (0. K))) by A1;
hence v + u in Solutions_of (A,(k |-> (0. K))) by A9, A11, MATRIX13:102; :: thesis: verum

end;

hence for b₁ being Subset of ((width A) -VectSp_over K) st b₁ = Solutions_of (A,(k |-> (0. K))) holds
b₁ is linearly-closed by A2, VECTSP_4:def 1; :: thesis: verum