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

A5: N = {} by A4;
assume the_rank_of A <> 0 ; :: thesis: contradiction
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:87;
A9: i in dom A by A6, ZFMISC_1:87;
then 0. K = ((len A) |-> (0. K)) . i by A3, FINSEQ_2:57
.= (Col (A,j)) . i by A2, A8, A5
.= A * (i,j) by A9, MATRIX_0:def 8 ;
hence contradiction by A7; :: 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 A10: card N > 0 ; :: thesis: the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N))

then N <> {} ;
then Seg (width A) <> {} by A1, XBOOLE_1:3;
then A11: width A <> 0 ;
then A12: len A <> 0 by MATRIX_0:def 3;
set AT = A @ ;
A13: [:(dom A),N:] c= Indices A by A1, ZFMISC_1:95;
A14: width (A @) = len A by A11, MATRIX_0:54;
A15: len (A @) = width A by A11, MATRIX_0:54;
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 :: thesis: for i being Nat st i in (dom (A @)) \ N holds
Line ((A @),i) = (width (A @)) |-> (0. K)

let i be Nat; :: thesis: ( i in (dom (A @)) \ N implies Line ((A @),i) = (width (A @)) |-> (0. K) )
assume A19: i in (dom (A @)) \ N ; :: thesis: Line ((A @),i) = (width (A @)) |-> (0. K)
i in dom (A @) by A19, XBOOLE_0:def 5;
hence Line ((A @),i) = Col (A,i) by A15, A17, MATRIX_0:59
.= (width (A @)) |-> (0. K) by A2, A15, A14, A17, A19 ;
:: 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 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: verum

end;

end;