let K be Field; :: thesis:
let A be Matrix of K; :: thesis:
let N be finite without_zero Subset of NAT ; :: thesis:
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:
A3: dom A = Seg (len A) by FINSEQ_1:def 3;

per cases ;

suppose A4: card N = 0 ; :: thesis:

the_rank_of A = 0

proof

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

end;

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

end;

suppose A10: card N > 0 ; :: thesis:

then N <> {} ;
then Seg (width A) <> {} by A1, XBOOLE_1:3;
then A11: width A <> 0 by A1, CARD_1:47, FINSEQ_1:4, XBOOLE_1:3;
then A12: len A <> 0 by MATRIX_1:def 4;
set AT = A @ ;
A13: [:(dom A),N:] c= Indices A by A1, ZFMISC_1:118;
A14: width (A @ ) = len A by A11, MATRIX_2:12;
A15: len (A @ ) = width A by A11, MATRIX_2:12;
then A16: N c= dom (A @ ) by A1, FINSEQ_1:def 3;
A17: dom (A @ ) = Seg (len (A @ )) by FINSEQ_1:def 3;

A18: now

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

end;

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

end;

end;