let m be Nat; :: thesis: for K being Field
for W being Subspace of m -VectSp_over K ex A being Matrix of dim W,m,K ex N being finite without_zero Subset of NAT 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 dim W,m,K ex N being finite without_zero Subset of NAT 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 dim W,m,K ex N being finite without_zero Subset of NAT 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 W such that
A1: I is Basis of W by MATRLIN:def 1;
I is linearly-independent by ;
then reconsider U = I as linearly-independent Subset of () by VECTSP_9:11;
defpred S1[ set , set ] means for A, B being Matrix of card I,m,K st \$1 = A holds
( A is without_repeated_line & lines A is linearly-independent & Lin () = (Omega). W );
deffunc H1( Matrix of card I,m,K, Nat, Nat, Element of K) -> Matrix of card I,m,K = \$1;
consider M being Matrix of card I,m,K such that
A2: ( M is without_repeated_line & lines M = U ) by MATRIX13:104;
A3: for A9, B9 being Matrix of card I,m,K st S1[A9,B9] holds
for a being Element of K
for i, j being Nat st j in dom A9 & ( i = j implies a <> - (1_ K) ) holds
S1[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H1(B9,i,j,a)]
proof
let A9, B9 be Matrix of card I,m,K; :: thesis: ( S1[A9,B9] implies for a being Element of K
for i, j being Nat st j in dom A9 & ( i = j implies a <> - (1_ K) ) holds
S1[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H1(B9,i,j,a)] )

assume A4: S1[A9,B9] ; :: thesis: for a being Element of K
for i, j being Nat st j in dom A9 & ( i = j implies a <> - (1_ K) ) holds
S1[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H1(B9,i,j,a)]

A5: dom A9 = Seg (len A9) by FINSEQ_1:def 3;
let a be Element of K; :: thesis: for i, j being Nat st j in dom A9 & ( i = j implies a <> - (1_ K) ) holds
S1[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H1(B9,i,j,a)]

let i, j be Nat; :: thesis: ( j in dom A9 & ( i = j implies a <> - (1_ K) ) implies S1[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H1(B9,i,j,a)] )
assume A6: ( j in dom A9 & ( i = j implies a <> - (1_ K) ) ) ; :: thesis: S1[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H1(B9,i,j,a)]
set R = RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))));
A7: A9 is without_repeated_line by A4;
then A8: Lin (lines A9) = Lin (lines (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))) by ;
lines A9 is linearly-independent by A4;
then card I = the_rank_of A9 by
.= the_rank_of (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) by ;
hence S1[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H1(B9,i,j,a)] by ; :: thesis: verum
end;
Lin I = ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) by ;
then A9: S1[M,M] by A2, VECTSP_9:17;
consider A9, B9 being Matrix of card I,m,K, N being finite without_zero Subset of NAT such that
A10: N c= Seg m and
A11: ( the_rank_of M = the_rank_of A9 & the_rank_of M = card N & S1[A9,B9] ) and
A12: Segm (A9,(Seg (card N)),N) = 1. (K,(card N)) and
for i being Nat st i in dom A9 & i > card N holds
Line (A9,i) = m |-> (0. K) and
for i, j being Nat st i in Seg (card N) & j in Seg (width A9) & j < (Sgm N) . i holds
A9 * (i,j) = 0. K from dim W = card I by ;
then reconsider A9 = A9 as Matrix of dim W,m,K ;
lines A9 c= the carrier of (Lin (lines A9)) by ;
then reconsider lA = lines A9 as linearly-independent Subset of W by ;
take A9 ; :: thesis: ex N being finite without_zero Subset of NAT st
( N c= Seg m & dim W = card N & Segm (A9,(Seg (dim W)),N) = 1. (K,(dim W)) & the_rank_of A9 = dim W & lines A9 is Basis of W )

take N ; :: thesis: ( N c= Seg m & dim W = card N & Segm (A9,(Seg (dim W)),N) = 1. (K,(dim W)) & the_rank_of A9 = dim W & lines A9 is Basis of W )
A13: Lin lA = Lin (lines A9) by VECTSP_9:17;
A14: the_rank_of M = card I by ;
A15: card I = dim W by ;
Lin (lines A9) = ModuleStr(# the carrier of W, the addF of W, the ZeroF of W, the lmult of W #) by A11;
hence ( N c= Seg m & dim W = card N & Segm (A9,(Seg (dim W)),N) = 1. (K,(dim W)) & the_rank_of A9 = dim W & lines A9 is Basis of W ) by ; :: thesis: verum