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 3;
I is linearly-independent by A1, VECTSP_7:def 3;
then reconsider U = I as linearly-independent Subset of (m -VectSp_over K) by VECTSP_9:15;
defpred S₁[ set , set ] means for A, B being Matrix of card I,m,K st $1 = A holds
( A is one-to-one & lines A is linearly-independent & Lin (lines A) = (Omega). W );
deffunc H₁( 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 one-to-one & lines M = U ) by MATRIX13:104;
A3: for A9, B9 being Matrix of card I,m,K st S₁[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
S₁[ RLine A9,i,((Line A9,i) + (a * (Line A9,j))),H₁(B9,i,j,a)]

proof

let A9, B9 be Matrix of card I,m,K; :: thesis: ( S₁[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
S₁[ RLine A9,i,((Line A9,i) + (a * (Line A9,j))),H₁(B9,i,j,a)] )
assume A4: S₁[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
S₁[ RLine A9,i,((Line A9,i) + (a * (Line A9,j))),H₁(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
S₁[ RLine A9,i,((Line A9,i) + (a * (Line A9,j))),H₁(B9,i,j,a)]
let i, j be Nat; :: thesis: ( j in dom A9 & ( i = j implies a <> - (1_ K) ) implies S₁[ RLine A9,i,((Line A9,i) + (a * (Line A9,j))),H₁(B9,i,j,a)] )
assume A6: ( j in dom A9 & ( i = j implies a <> - (1_ K) ) ) ; :: thesis: S₁[ RLine A9,i,((Line A9,i) + (a * (Line A9,j))),H₁(B9,i,j,a)]
set R = RLine A9,i,((Line A9,i) + (a * (Line A9,j)));
A7: A9 is one-to-one by A4;
then A8: Lin (lines A9) = Lin (lines (RLine A9,i,((Line A9,i) + (a * (Line A9,j))))) by A6, Th69;
lines A9 is linearly-independent by A4;
then card I = the_rank_of A9 by A7, MATRIX13:121
.= the_rank_of (RLine A9,i,((Line A9,i) + (a * (Line A9,j)))) by A6, A5, MATRIX13:92 ;
hence S₁[ RLine A9,i,((Line A9,i) + (a * (Line A9,j))),H₁(B9,i,j,a)] by A4, A8, MATRIX13:121; :: thesis: verum

end;

Lin I = VectSpStr(# the carrier of W,the addF of W,the ZeroF of W,the lmult of W #) by A1, VECTSP_7:def 3;
then A9: S₁[M,M] by A2, VECTSP_9:21;
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 & S₁[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 MATRIX15:sch 2(A9, A3);
reconsider A9 = A9 as Matrix of dim W,m,K by A1, VECTSP_9:def 2;
lines A9 c= the carrier of (Lin (lines A9))

proof

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

end;

then reconsider lA = lines A9 as linearly-independent Subset of W by A11, VECTSP_9:16;
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: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 A9) = VectSpStr(# 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 A15, A10, A11, A12, A14, A13, VECTSP_7:def 3; :: thesis: verum