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_{1}[ 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_{1}( 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_{1}[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_{1}[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H_{1}(B9,i,j,a)]

then A9: S_{1}[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_{1}[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

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

( A is without_repeated_line & lines A is linearly-independent & Lin (lines A) = (Omega). W );

deffunc H

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

for a being Element of K

for i, j being Nat st j in dom A9 & ( i = j implies a <> - (1_ K) ) holds

S

proof

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;
let A9, B9 be Matrix of card I,m,K; :: thesis: ( S_{1}[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_{1}[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H_{1}(B9,i,j,a)] )

assume A4: S_{1}[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_{1}[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H_{1}(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_{1}[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H_{1}(B9,i,j,a)]

let i, j be Nat; :: thesis: ( j in dom A9 & ( i = j implies a <> - (1_ K) ) implies S_{1}[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H_{1}(B9,i,j,a)] )

assume A6: ( j in dom A9 & ( i = j implies a <> - (1_ K) ) ) ; :: thesis: S_{1}[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H_{1}(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_{1}[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),H_{1}(B9,i,j,a)]
by A4, A8, MATRIX13:121; :: thesis: verum

end;for i, j being Nat st j in dom A9 & ( i = j implies a <> - (1_ K) ) holds

S

assume A4: S

for i, j being Nat st j in dom A9 & ( i = j implies a <> - (1_ K) ) holds

S

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

let i, j be Nat; :: thesis: ( j in dom A9 & ( i = j implies a <> - (1_ K) ) implies S

assume A6: ( j in dom A9 & ( i = j implies a <> - (1_ K) ) ) ; :: thesis: S

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

then A9: S

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

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