let K be Field; :: thesis: for A being Matrix of K
for N being finite without_zero Subset of NAT st N c= Seg (width A) & ( for i being Nat st i in (Seg (width A)) \ N holds
Col A,i = (len A) |-> (0. K) ) holds
the_rank_of A = the_rank_of (Segm A,(Seg (len A)),N)
let A be Matrix of K; :: thesis: for N being finite without_zero Subset of NAT st N c= Seg (width A) & ( for i being Nat st i in (Seg (width A)) \ N holds
Col A,i = (len A) |-> (0. K) ) holds
the_rank_of A = the_rank_of (Segm A,(Seg (len A)),N)
let N be finite without_zero Subset of NAT ; :: thesis: ( N c= Seg (width A) & ( for i being Nat st i in (Seg (width A)) \ N holds
Col A,i = (len A) |-> (0. K) ) implies the_rank_of A = the_rank_of (Segm A,(Seg (len A)),N) )
assume that
A1: N c= Seg (width A) and
A2: for i being Nat st i in (Seg (width A)) \ N holds
Col A,i = (len A) |-> (0. K) ; :: thesis: the_rank_of A = the_rank_of (Segm A,(Seg (len A)),N)
A3: dom A = Seg (len A) by FINSEQ_1:def 3;

per cases ( card N = 0 or card N > 0 ) ;

suppose A4: card N = 0 ; :: thesis: the_rank_of A = the_rank_of (Segm A,(Seg (len A)),N)

the_rank_of A = 0

proof

assume the_rank_of A <> 0 ; :: thesis: contradiction
then the_rank_of A > 0 ;
then consider i, j being Nat such that
A5: ( [i,j] in Indices A & A * i,j <> 0. K ) by MATRIX13:94;
A6: ( i in dom A & j in Seg (width A) & N = {} ) by A4, A5, ZFMISC_1:106;
then 0. K = ((len A) |-> (0. K)) . i by A3, FINSEQ_2:71
.= (Col A,j) . i by A2, A6
.= A * i,j by A6, MATRIX_1:def 9 ;
hence contradiction by A5; :: thesis: verum

end;

hence the_rank_of A = the_rank_of (Segm A,(Seg (len A)),N) by A4, MATRIX13:77; :: thesis: verum

end;

suppose A7: card N > 0 ; :: thesis: the_rank_of A = the_rank_of (Segm A,(Seg (len A)),N)

then A8: width A <> 0 by A1, CARD_1:47, FINSEQ_1:4, XBOOLE_1:3;
then len A <> 0 by MATRIX_1:def 4;
then len A in Seg (len A) by FINSEQ_1:5;
then A9: ( card (Seg (len A)) = 0 iff card N = 0 ) by A7;
A10: [:(dom A),N:] c= Indices A by A1, ZFMISC_1:118;
set AT = A @ ;
A11: width A > 0 by A8;
then A12: len (A @ ) = width A by MATRIX_2:12;
A13: width (A @ ) = len A by A11, MATRIX_2:12;
A14: dom (A @ ) = Seg (len (A @ )) by FINSEQ_1:def 3;
A15: N c= dom (A @ ) by A1, A12, FINSEQ_1:def 3;

A16: now

let i be Nat; :: thesis: ( i in (dom (A @ )) \ N implies Line (A @ ),i = (width (A @ )) |-> (0. K) )
assume A17: i in (dom (A @ )) \ N ; :: thesis: Line (A @ ),i = (width (A @ )) |-> (0. K)
i in dom (A @ ) by A17, XBOOLE_0:def 5;
hence Line (A @ ),i = Col A,i by A12, A14, MATRIX_2:17
.= (width (A @ )) |-> (0. K) by A2, A12, A13, A14, A17 ;
:: thesis: verum

end;

thus the_rank_of A = the_rank_of (A @ ) by MATRIX13:84
.= the_rank_of (Segm (A @ ),N,(Seg (len A))) by A13, A15, A16, Th11
.= the_rank_of ((Segm A,(Seg (len A)),N) @ ) by A10, A9, A3, MATRIX13:61
.= the_rank_of (Segm A,(Seg (len A)),N) by MATRIX13:84 ; :: thesis: verum

end;

end;