set V = () -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 (() -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 (() -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 (() -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 () -tuples_on the carrier of K by ;
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
.= (a * (0. K)) * (0. (K,k,1)) by MATRIX_5:11
.= (0. K) * (0. (K,k,1))
.= 0. (K,k,1) by ;
:: thesis: verum
end;
end;
end;
then a * () 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 ; :: thesis: verum
end;
now :: thesis: for v, u being Element of (() -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 (() -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 ;
reconsider f = f, g = g as Element of () -tuples_on the carrier of K by ;
(ColVec2Mx f) + () in Solutions_of (A,((0. (K,k,1)) + (0. (K,k,1)))) by A1, A10, A12, Th37;
then (ColVec2Mx f) + () 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 ;
then f + g in Solutions_of (A,(k |-> (0. K))) by A1;
hence v + u in Solutions_of (A,(k |-> (0. K))) by ; :: thesis: verum
end;
hence for b1 being Subset of (() -VectSp_over K) st b1 = Solutions_of (A,(k |-> (0. K))) holds
b1 is linearly-closed by ; :: thesis: verum