let K be Field; :: thesis: for A being Matrix of K
for N being finite without_zero Subset of NAT st N c= Seg () & ( for i being Nat st i in (Seg ()) \ 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 () & ( for i being Nat st i in (Seg ()) \ 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 () & ( for i being Nat st i in (Seg ()) \ 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 () and
A2: for i being Nat st i in (Seg ()) \ 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 () by ;
A9: i in dom A by ;
then 0. K = ((len A) |-> (0. K)) . i by
.= (Col (A,j)) . i by A2, A8, A5
.= A * (i,j) by ;
hence contradiction by A7; :: thesis: verum
end;
hence the_rank_of A = the_rank_of (Segm (A,(Seg (len A)),N)) by ; :: 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 () <> {} by ;
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 ;
A14: width (A @) = len A by ;
A15: len (A @) = width A by ;
then A16: N c= dom (A @) by ;
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 ;
hence Line ((A @),i) = Col (A,i) by
.= (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
.= the_rank_of ((Segm (A,(Seg (len A)),N)) @) by
.= the_rank_of (Segm (A,(Seg (len A)),N)) by MATRIX13:84 ; :: thesis: verum
end;
end;