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 A1, VECTSP_7:def 3;
then reconsider U = I as linearly-independent Subset of (m -VectSp_over K) by VECTSP_9:11;
defpred S₁[ 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 (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 without_repeated_line & 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 without_repeated_line 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 = ModuleStr(# 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: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 & 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);
dim W = card I by A1, VECTSP_9:def 1;
then reconsider A9 = A9 as Matrix of dim W,m,K ;
lines A9 c= the carrier of (Lin (lines A9)) by VECTSP_7:8, STRUCT_0:def 5;
then reconsider lA = lines A9 as linearly-independent Subset of W by A11, VECTSP_9:12;
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 A2, MATRIX13:121;
A15: card I = dim W by A1, VECTSP_9:def 1;
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 A15, A10, A11, A12, A14, A13, VECTSP_7:def 3; :: thesis: verum