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;

_{1} being Subset of ((width A) -VectSp_over K) st b_{1} = Solutions_of (A,(k |-> (0. K))) holds

b_{1} is linearly-closed
by A2, VECTSP_4:def 1; :: thesis: verum

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)))

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;

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;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))end;

then
a * (ColVec2Mx f) in Solutions_of (A,(0. (K,k,1)))
by A1, A4, Th35;per cases
( k = 0 or k > 0 )
;

end;

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;hence 0. (K,k,1) = a * (0. (K,k,1)) ; :: thesis: verum

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

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

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)))

hence
for bv + 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;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

b