let m be Nat; :: thesis: for K being Field
for W being Subspace of m -VectSp_over K ex A being Matrix of the carrier of K, dim W, ex N being finite without_zero Subset of st
( N c= Seg m & dim W = card N & Segm A,(Seg (dim W)),N = 1. K,(dim W) & the_rank_of A = dim W & lines A is Basis of W )
let K be Field; :: thesis: for W being Subspace of m -VectSp_over K ex A being Matrix of the carrier of K, dim W, ex N being finite without_zero Subset of st
( N c= Seg m & dim W = card N & Segm A,(Seg (dim W)),N = 1. K,(dim W) & the_rank_of A = dim W & lines A is Basis of W )
let W be Subspace of m -VectSp_over K; :: thesis: ex A being Matrix of the carrier of K, dim W, ex N being finite without_zero Subset of st
( N c= Seg m & dim W = card N & Segm A,(Seg (dim W)),N = 1. K,(dim W) & the_rank_of A = dim W & lines A is Basis of W )
consider I being finite Subset of such that
A1: I is Basis of W by MATRLIN:def 3;
I is linearly-independent by A1, VECTSP_7:def 3;
then reconsider U = I as linearly-independent Subset of by VECTSP_9:15;
defpred S₁[ set , set ] means for A, B being Matrix of the carrier of K, card I, st $1 = A holds
( A is one-to-one & lines A is linearly-independent & Lin (lines A) = (Omega). W );
deffunc H₁( Matrix of the carrier of K, card I,, Nat, Nat, Element of ) -> Matrix of the carrier of K, card I, = $1;
consider M being Matrix of the carrier of K, card I, such that
A2: ( M is one-to-one & lines M = U ) by MATRIX13:104;
A3: for A', B' being Matrix of the carrier of K, card I, st S₁[A',B'] holds
for a being Element of
for i, j being Nat st j in dom A' & ( i = j implies a <> - (1_ K) ) holds
S₁[ RLine A',i,((Line A',i) + (a * (Line A',j))),H₁(B',i,j,a)]

proof

let A', B' be Matrix of the carrier of K, card I,; :: thesis: ( S₁[A',B'] implies for a being Element of
for i, j being Nat st j in dom A' & ( i = j implies a <> - (1_ K) ) holds
S₁[ RLine A',i,((Line A',i) + (a * (Line A',j))),H₁(B',i,j,a)] )
assume A4: S₁[A',B'] ; :: thesis: for a being Element of
for i, j being Nat st j in dom A' & ( i = j implies a <> - (1_ K) ) holds
S₁[ RLine A',i,((Line A',i) + (a * (Line A',j))),H₁(B',i,j,a)]
A5: dom A' = Seg (len A') by FINSEQ_1:def 3;
let a be Element of ; :: thesis: for i, j being Nat st j in dom A' & ( i = j implies a <> - (1_ K) ) holds
S₁[ RLine A',i,((Line A',i) + (a * (Line A',j))),H₁(B',i,j,a)]
let i, j be Nat; :: thesis: ( j in dom A' & ( i = j implies a <> - (1_ K) ) implies S₁[ RLine A',i,((Line A',i) + (a * (Line A',j))),H₁(B',i,j,a)] )
assume A6: ( j in dom A' & ( i = j implies a <> - (1_ K) ) ) ; :: thesis: S₁[ RLine A',i,((Line A',i) + (a * (Line A',j))),H₁(B',i,j,a)]
set R = RLine A',i,((Line A',i) + (a * (Line A',j)));
A7: A' is one-to-one by A4;
then A8: Lin (lines A') = Lin (lines (RLine A',i,((Line A',i) + (a * (Line A',j))))) by A6, Th69;
lines A' is linearly-independent by A4;
then card I = the_rank_of A' by A7, MATRIX13:121
.= the_rank_of (RLine A',i,((Line A',i) + (a * (Line A',j)))) by A6, A5, MATRIX13:92 ;
hence S₁[ RLine A',i,((Line A',i) + (a * (Line A',j))),H₁(B',i,j,a)] by A4, A8, MATRIX13:121; :: thesis: verum

end;

Lin I = VectSpStr(# the carrier of W,the addF of W,the U2 of W,the lmult of W #) by A1, VECTSP_7:def 3;
then A9: S₁[M,M] by A2, VECTSP_9:21;
consider A', B' being Matrix of the carrier of K, card I,, N being finite without_zero Subset of such that
A10: N c= Seg m and
A11: ( the_rank_of M = the_rank_of A' & the_rank_of M = card N & S₁[A',B'] ) and
A12: Segm A',(Seg (card N)),N = 1. K,(card N) and
for i being Nat st i in dom A' & i > card N holds
Line A',i = m |-> (0. K) and
for i, j being Nat st i in Seg (card N) & j in Seg (width A') & j < (Sgm N) . i holds
A' * i,j = 0. K from MATRIX15:sch 2(A9, A3);
reconsider A' = A' as Matrix of the carrier of K, dim W, by A1, VECTSP_9:def 2;
lines A' c= the carrier of (Lin (lines A'))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in lines A' or x in the carrier of (Lin (lines A')) )
assume x in lines A' ; :: thesis: x in the carrier of (Lin (lines A'))
then x in Lin (lines A') by VECTSP_7:13;
hence x in the carrier of (Lin (lines A')) by STRUCT_0:def 5; :: thesis: verum

end;

then reconsider lA = lines A' as linearly-independent Subset of by A11, VECTSP_9:16;
take A' ; :: thesis: ex N being finite without_zero Subset of st
( N c= Seg m & dim W = card N & Segm A',(Seg (dim W)),N = 1. K,(dim W) & the_rank_of A' = dim W & lines A' is Basis of W )
take N ; :: thesis: ( N c= Seg m & dim W = card N & Segm A',(Seg (dim W)),N = 1. K,(dim W) & the_rank_of A' = dim W & lines A' is Basis of W )
A13: Lin lA = Lin (lines A') by VECTSP_9:21;
A14: the_rank_of M = card I by A2, MATRIX13:121;
A15: card I = dim W by A1, VECTSP_9:def 2;
Lin (lines A') = VectSpStr(# the carrier of W,the addF of W,the U2 of W,the lmult of W #) by A11;
hence ( N c= Seg m & dim W = card N & Segm A',(Seg (dim W)),N = 1. K,(dim W) & the_rank_of A' = dim W & lines A' is Basis of W ) by A15, A10, A11, A12, A14, A13, VECTSP_7:def 3; :: thesis: verum