let K be Field; :: thesis: for A being Matrix of K
for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in (dom A) \ N holds
Line A,i = (width A) |-> (0. K) ) holds
the_rank_of A = the_rank_of (Segm A,N,(Seg (width A)))
let A be Matrix of K; :: thesis: for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in (dom A) \ N holds
Line A,i = (width A) |-> (0. K) ) holds
the_rank_of A = the_rank_of (Segm A,N,(Seg (width A)))
let N be finite without_zero Subset of NAT ; :: thesis: ( N c= dom A & ( for i being Nat st i in (dom A) \ N holds
Line A,i = (width A) |-> (0. K) ) implies the_rank_of A = the_rank_of (Segm A,N,(Seg (width A))) )
assume that
A1: N c= dom A and
A2: for i being Nat st i in (dom A) \ N holds
Line A,i = (width A) |-> (0. K) ; :: thesis: the_rank_of A = the_rank_of (Segm A,N,(Seg (width A)))
reconsider A' = A as Matrix of len A, width A,K by MATRIX_2:7;
set l = len A;
set w = width A;
set S = Segm A',N,(Seg (width A'));
consider U being finite Subset of ((width A) -VectSp_over K) such that
A3: ( U is linearly-independent & U c= lines A' & card U = the_rank_of A' ) by MATRIX13:123;
A4: U c= lines (Segm A',N,(Seg (width A')))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in U or x in lines (Segm A',N,(Seg (width A'))) )
assume A5: x in U ; :: thesis: x in lines (Segm A',N,(Seg (width A')))
consider Ni being Nat such that
A6: ( Ni in Seg (len A) & x = Line A',Ni ) by A3, A5, MATRIX13:103;
A7: dom A = Seg (len A) by FINSEQ_1:def 3;
A8: Ni in N

proof

assume not Ni in N ; :: thesis: contradiction
then Ni in (dom A) \ N by A6, A7, XBOOLE_0:def 5;
then x = (width A) |-> (0. K) by A2, A6
.= 0. ((width A) -VectSp_over K) by MATRIX13:102 ;
hence contradiction by A3, A5, VECTSP_7:3; :: thesis: verum

end;

rng (Sgm N) = N by A1, A7, FINSEQ_1:def 13;
then consider i being set such that
A9: ( i in dom (Sgm N) & (Sgm N) . i = Ni ) by A8, FUNCT_1:def 5;
reconsider i = i as Element of NAT by A9;
A10: dom (Sgm N) = Seg (card N) by A1, A7, FINSEQ_3:45;
then Line (Segm A',N,(Seg (width A'))),i = x by A6, A9, MATRIX13:48;
hence x in lines (Segm A',N,(Seg (width A'))) by A9, A10, MATRIX13:103; :: thesis: verum

end;

A11: width A = card (Seg (width A)) by FINSEQ_1:78;

now

let W be finite Subset of ((width A) -VectSp_over K); :: thesis: ( W is linearly-independent & W c= lines (Segm A',N,(Seg (width A'))) implies card W <= the_rank_of A' )
assume A12: ( W is linearly-independent & W c= lines (Segm A',N,(Seg (width A'))) ) ; :: thesis: card W <= the_rank_of A'
dom A = Seg (len A) by FINSEQ_1:def 3;
then lines (Segm A',N,(Seg (width A'))) c= lines A' by A1, MATRIX13:118;
then W c= lines A' by A12, XBOOLE_1:1;
hence card W <= the_rank_of A' by A12, MATRIX13:123; :: thesis: verum

end;

hence the_rank_of A = the_rank_of (Segm A,N,(Seg (width A))) by A3, A4, A11, MATRIX13:123; :: thesis: verum