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) = () |-> (0. K) ) holds
the_rank_of A = the_rank_of (Segm (A,N,(Seg ())))

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) = () |-> (0. K) ) holds
the_rank_of A = the_rank_of (Segm (A,N,(Seg ())))

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) = () |-> (0. K) ) implies the_rank_of A = the_rank_of (Segm (A,N,(Seg ()))) )

assume that
A1: N c= dom A and
A2: for i being Nat st i in (dom A) \ N holds
Line (A,i) = () |-> (0. K) ; :: thesis: the_rank_of A = the_rank_of (Segm (A,N,(Seg ())))
set w = width A;
set l = len A;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;
set S = Segm (A9,N,(Seg (width A9)));
consider U being finite Subset of (() -VectSp_over K) such that
A3: U is linearly-independent and
A4: U c= lines A9 and
A5: card U = the_rank_of A9 by MATRIX13:123;
A6: U c= lines (Segm (A9,N,(Seg (width A9))))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in U or x in lines (Segm (A9,N,(Seg (width A9)))) )
assume A7: x in U ; :: thesis: x in lines (Segm (A9,N,(Seg (width A9))))
consider Ni being Nat such that
A8: Ni in Seg (len A) and
A9: x = Line (A9,Ni) by ;
A10: dom A = Seg (len A) by FINSEQ_1:def 3;
A11: Ni in N
proof
assume not Ni in N ; :: thesis: contradiction
then Ni in (dom A) \ N by ;
then x = () |-> (0. K) by A2, A9
.= 0. (() -VectSp_over K) by MATRIX13:102 ;
hence contradiction by A3, A7, VECTSP_7:2; :: thesis: verum
end;
rng (Sgm N) = N by ;
then consider i being object such that
A12: i in dom (Sgm N) and
A13: (Sgm N) . i = Ni by ;
reconsider i = i as Element of NAT by A12;
A14: dom (Sgm N) = Seg (card N) by ;
then Line ((Segm (A9,N,(Seg (width A9)))),i) = x by ;
hence x in lines (Segm (A9,N,(Seg (width A9)))) by ; :: thesis: verum
end;
A15: now :: thesis: for W being finite Subset of (() -VectSp_over K) st W is linearly-independent & W c= lines (Segm (A9,N,(Seg (width A9)))) holds
card W <= the_rank_of A9
let W be finite Subset of (() -VectSp_over K); :: thesis: ( W is linearly-independent & W c= lines (Segm (A9,N,(Seg (width A9)))) implies card W <= the_rank_of A9 )
assume that
A16: W is linearly-independent and
A17: W c= lines (Segm (A9,N,(Seg (width A9)))) ; :: thesis:
dom A = Seg (len A) by FINSEQ_1:def 3;
then lines (Segm (A9,N,(Seg (width A9)))) c= lines A9 by ;
then W c= lines A9 by A17;
hence card W <= the_rank_of A9 by ; :: thesis: verum
end;
width A = card (Seg ()) by FINSEQ_1:57;
hence the_rank_of A = the_rank_of (Segm (A,N,(Seg ()))) by ; :: thesis: verum