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 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;
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);
( 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)))
;
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 0. (K,k,1) = a * (0. (K,k,1))per cases
( k = 0 or k > 0 )
;
suppose
k = 0
;
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))
;
verum end; suppose A5:
k > 0
;
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
;
verum 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;
verum end;
now 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);
( 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)))
;
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;
verum end;
hence
for b1 being Subset of ((width A) -VectSp_over K) st b1 = Solutions_of (A,(k |-> (0. K))) holds
b1 is linearly-closed
by A2, VECTSP_4:def 1; verum