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

A2: 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 A3: ( v in Solutions_of A,(k |-> (0. K)) & 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
A4: ( v = f & ColVec2Mx f in Solutions_of A,(ColVec2Mx (k |-> (0. K))) ) by A3;
consider g being FinSequence of K such that
A5: ( u = g & ColVec2Mx g in Solutions_of A,(ColVec2Mx (k |-> (0. K))) ) by A3;
A6: ( len g = width A & len f = width A ) by A4, A5, Th59;
reconsider f = f, g = g as Element of (width A) -tuples_on the carrier of K by A4, A5, MATRIX13:102;
(ColVec2Mx f) + (ColVec2Mx g) in Solutions_of A,((0. K,k,1) + (0. K,k,1)) by A4, A5, Th37, A1;
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 A6, Th28;
then f + g in Solutions_of A,(k |-> (0. K)) by A1;
hence v + u in Solutions_of A,(k |-> (0. K)) by A4, A5, MATRIX13:102; :: thesis: verum

end;

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 A7: v in Solutions_of A,(k |-> (0. K)) ; :: thesis: a * v in Solutions_of A,(k |-> (0. K))
consider f being FinSequence of K such that
A8: ( v = f & ColVec2Mx f in Solutions_of A,(ColVec2Mx (k |-> (0. K))) ) by A7;
reconsider f = f as Element of (width A) -tuples_on the carrier of K by A8, 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 (0. K,k,1) = 0 & len (a * (0. K,k,1)) = len (0. K,k,1) ) by MATRIX_3:def 5;
then ( 0. K,k,1 = {} & a * (0. K,k,1) = {} ) ;
hence 0. K,k,1 = a * (0. K,k,1) ; :: thesis: verum

end;

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

then A10: ( 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 A9, 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 A9, A10, MATRIX_5:40 ;
:: thesis: verum

end;

end;

end;

then a * (ColVec2Mx f) in Solutions_of A,(0. K,k,1) by A8, A1, 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 A8, 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