let m, n 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))

A3: dom mt = Seg m by FINSEQ_2:124;
A4: dom nt = Seg n by FINSEQ_2:124;
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
A5: [:(rng rt1),(rng rt2):] c= Indices (Segm (M,nt,mt)) and
A6: Det (Segm ((Segm (M,nt,mt)),rt1,rt2)) <> 0. K by Th76;
set mr = mt * rt2;
A7: ex R1, R2 being finite without_zero Subset of NAT st
( R1 = rng rt1 & R2 = rng rt2 & card R1 = card R2 & card R1 = the_rank_of (Segm (M,nt,mt)) & Det (EqSegm ((Segm (M,nt,mt)),R1,R2)) <> 0. K ) by A5, A6, Th75;
set nr = nt * rt1;
A8: rng (mt * rt2) c= rng mt by RELAT_1:26;
len (Segm (M,nt,mt)) = n by A2, Th1;
then A9: rng rt1 c= dom nt by A5, A7, A4, Th67;
then dom (nt * rt1) = dom rt1 by RELAT_1:27;
then A10: dom (nt * rt1) = Seg (the_rank_of (Segm (M,nt,mt))) by FINSEQ_2:124;
width (Segm (M,nt,mt)) = m by A2, Th1;
then A11: rng rt2 c= dom mt by A5, A7, A3, Th67;
then dom (mt * rt2) = dom rt2 by RELAT_1:27;
then A12: dom (mt * rt2) = Seg (the_rank_of (Segm (M,nt,mt))) by FINSEQ_2:124;
rng mt c= NAT by FINSEQ_1:def 4;
then A13: rng (mt * rt2) c= NAT by A8;
set SS = Segm ((Segm (M,nt,mt)),rt1,rt2);
A14: rng (nt * rt1) c= rng nt by RELAT_1:26;
rng nt c= NAT by FINSEQ_1:def 4;
then A15: rng (nt * rt1) c= NAT by A14;
reconsider nr = nt * rt1, mr = mt * rt2 as FinSequence by A9, A11, FINSEQ_1:16;
reconsider nr = nr, mr = mr as FinSequence of NAT by A15, A13, FINSEQ_1:def 4;
A16: len nr = the_rank_of (Segm (M,nt,mt)) by A10, FINSEQ_1:def 3;
len mr = the_rank_of (Segm (M,nt,mt)) by A12, FINSEQ_1:def 3;
then reconsider nr = nr, mr = mr as Element of (the_rank_of (Segm (M,nt,mt))) -tuples_on NAT by A16, FINSEQ_2:92;
set MR = Segm (M,nr,mr);

now :: thesis: for i, j being Nat st [i,j] in Indices (Segm ((Segm (M,nt,mt)),rt1,rt2)) holds
(Segm (M,nr,mr)) * (i,j) = (Segm ((Segm (M,nt,mt)),rt1,rt2)) * (i,j)

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 A17: [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 12;
A18: [(rt1 . I),(rt2 . J)] in Indices (Segm (M,nt,mt)) by A5, A17, Th17;
A19: Indices (Segm ((Segm (M,nt,mt)),rt1,rt2)) = [:(dom nr),(dom mr):] by A10, A12, MATRIX_0:24;
then A20: i in dom nr by A17, ZFMISC_1:87;
A21: j in dom mr by A17, A19, ZFMISC_1:87;
[i,j] in Indices (Segm (M,nr,mr)) by A17, MATRIX_0:26;
hence (Segm (M,nr,mr)) * (i,j) = M * ((nr . I),(mr . J)) by Def1
.= M * ((nt . rtI),(mr . J)) by A20, FUNCT_1:12
.= M * ((nt . rtI),(mt . rtJ)) by A21, FUNCT_1:12
.= (Segm (M,nt,mt)) * ((rt1 . I),(rt2 . J)) by A18, Def1
.= (Segm ((Segm (M,nt,mt)),rt1,rt2)) * (i,j) by A17, Def1 ;
:: thesis: verum

end;

then A22: Segm ((Segm (M,nt,mt)),rt1,rt2) = Segm (M,nr,mr) by MATRIX_0:27;
[:(rng nr),(rng mr):] c= [:(rng nt),(rng mt):] by A14, A8, ZFMISC_1:96;
then [:(rng nr),(rng mr):] c= Indices M by A1;
hence the_rank_of M >= the_rank_of (Segm (M,nt,mt)) by A6, A22, Th76; :: thesis: verum

end;

end;