let n, m be Nat; :: thesis: for K being Field
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
the_rank_of M >= the_rank_of (Segm M,nt,mt)
let K be Field; :: thesis: for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
the_rank_of M >= the_rank_of (Segm M,nt,mt)
let nt be Element of n -tuples_on NAT ; :: thesis: for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
the_rank_of M >= the_rank_of (Segm M,nt,mt)
let mt be Element of m -tuples_on NAT ; :: thesis: for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
the_rank_of M >= the_rank_of (Segm M,nt,mt)
let M be Matrix of K; :: thesis: ( [:(rng nt),(rng mt):] c= Indices M implies the_rank_of M >= the_rank_of (Segm M,nt,mt) )
assume A1: [:(rng nt),(rng mt):] c= Indices M ; :: thesis: the_rank_of M >= the_rank_of (Segm M,nt,mt)

per cases ( n = 0 or m = 0 or ( n > 0 & m > 0 ) ) ;

suppose ( n = 0 or m = 0 ) ; :: thesis: the_rank_of M >= the_rank_of (Segm M,nt,mt)

hence the_rank_of M >= the_rank_of (Segm M,nt,mt) by Th77; :: thesis: verum

end;

suppose A2: ( n > 0 & m > 0 ) ; :: thesis: the_rank_of M >= the_rank_of (Segm M,nt,mt)

set S = Segm M,nt,mt;
set RS = the_rank_of (Segm M,nt,mt);
consider rt1, rt2 being Element of (the_rank_of (Segm M,nt,mt)) -tuples_on NAT such that
A3: ( [:(rng rt1),(rng rt2):] c= Indices (Segm M,nt,mt) & Det (Segm (Segm M,nt,mt),rt1,rt2) <> 0. K ) by Th76;
consider R1, R2 being finite without_zero Subset of NAT such that
A4: ( R1 = rng rt1 & R2 = rng rt2 ) and
A5: ( card R1 = card R2 & card R1 = the_rank_of (Segm M,nt,mt) ) and
Det (EqSegm (Segm M,nt,mt),R1,R2) <> 0. K by A3, Th75;
set nr = nt * rt1;
set mr = mt * rt2;
( len (Segm M,nt,mt) = n & width (Segm M,nt,mt) = m & dom nt = Seg n & dom mt = Seg m ) by A2, Th1, FINSEQ_2:144;
then A6: ( rng rt1 c= dom nt & rng rt2 c= dom mt ) by A3, A4, A5, Th67;
then A7: ( dom (nt * rt1) = dom rt1 & rng (nt * rt1) c= rng nt & rng nt c= NAT & dom (mt * rt2) = dom rt2 & rng (mt * rt2) c= rng mt & rng mt c= NAT ) by FINSEQ_1:def 4, RELAT_1:45, RELAT_1:46;
then A8: ( dom (nt * rt1) = Seg (the_rank_of (Segm M,nt,mt)) & rng (nt * rt1) c= NAT & dom (mt * rt2) = Seg (the_rank_of (Segm M,nt,mt)) & rng (mt * rt2) c= NAT ) by FINSEQ_2:144, XBOOLE_1:1;
reconsider nr = nt * rt1, mr = mt * rt2 as FinSequence by A6, FINSEQ_1:20;
reconsider nr = nr, mr = mr as FinSequence of NAT by A8, FINSEQ_1:def 4;
( len nr = the_rank_of (Segm M,nt,mt) & len mr = the_rank_of (Segm M,nt,mt) ) by A8, FINSEQ_1:def 3;
then reconsider nr = nr, mr = mr as Element of (the_rank_of (Segm M,nt,mt)) -tuples_on NAT by FINSEQ_2:110;
set SS = Segm (Segm M,nt,mt),rt1,rt2;
set MR = Segm M,nr,mr;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm (Segm M,nt,mt),rt1,rt2) implies (Segm M,nr,mr) * i,j = (Segm (Segm M,nt,mt),rt1,rt2) * i,j )
assume A9: [i,j] in Indices (Segm (Segm M,nt,mt),rt1,rt2) ; :: thesis: (Segm M,nr,mr) * i,j = (Segm (Segm M,nt,mt),rt1,rt2) * i,j
reconsider I = i, J = j, rtI = rt1 . i, rtJ = rt2 . j as Element of NAT by ORDINAL1:def 13;
A10: [(rt1 . I),(rt2 . J)] in Indices (Segm M,nt,mt) by A3, A9, Th17;
Indices (Segm (Segm M,nt,mt),rt1,rt2) = [:(dom nr),(dom mr):] by A8, MATRIX_1:25;
then A11: ( i in dom nr & j in dom mr & [i,j] in Indices (Segm M,nr,mr) ) by A9, MATRIX_1:27, ZFMISC_1:106;
hence (Segm M,nr,mr) * i,j = M * (nr . I),(mr . J) by Def1
.= M * (nt . rtI),(mr . J) by A11, FUNCT_1:22
.= M * (nt . rtI),(mt . rtJ) by A11, FUNCT_1:22
.= (Segm M,nt,mt) * (rt1 . I),(rt2 . J) by A10, Def1
.= (Segm (Segm M,nt,mt),rt1,rt2) * i,j by A9, Def1 ;
:: thesis: verum

end;

then A12: Segm (Segm M,nt,mt),rt1,rt2 = Segm M,nr,mr by MATRIX_1:28;
[:(rng nr),(rng mr):] c= [:(rng nt),(rng mt):] by A7, ZFMISC_1:119;
then [:(rng nr),(rng mr):] c= Indices M by A1, XBOOLE_1:1;
hence the_rank_of M >= the_rank_of (Segm M,nt,mt) by A3, A12, Th76; :: thesis: verum

end;

end;