let K be Field; :: thesis: for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds
the_rank_of M >= the_rank_of (Segm (M,P,Q))
let M be Matrix of K; :: thesis: for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds
the_rank_of M >= the_rank_of (Segm (M,P,Q))
let P, Q be finite without_zero Subset of NAT; :: thesis: ( [:P,Q:] c= Indices M implies the_rank_of M >= the_rank_of (Segm (M,P,Q)) )
ex k being Nat st P c= Seg k by Th43;
then A1: rng (Sgm P) = P by FINSEQ_1:def 13;
ex n being Nat st Q c= Seg n by Th43;
then A2: rng (Sgm Q) = Q by FINSEQ_1:def 13;
assume [:P,Q:] c= Indices M ; :: thesis: the_rank_of M >= the_rank_of (Segm (M,P,Q))
hence the_rank_of M >= the_rank_of (Segm (M,P,Q)) by A1, A2, Th78; :: thesis: verum