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

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

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_1:24;
hence a * (0. K,k,1) = a * ((0. K) * (0. K,k,1)) by A5, MATRIX_5:40
.= (a * (0. K)) * (0. K,k,1) by MATRIX_5:12
.= (0. K) * (0. K,k,1) by VECTSP_1:36
.= 0. K,k,1 by A5, A6, MATRIX_5:40 ;
:: 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

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:6;
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