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)

A3: dom mt = Seg m by FINSEQ_2:144;
A4: dom nt = Seg n by FINSEQ_2:144;
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:45;
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:46;
then A10: dom (nt * rt1) = Seg (the_rank_of (Segm M,nt,mt)) by FINSEQ_2:144;
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:46;
then A12: dom (mt * rt2) = Seg (the_rank_of (Segm M,nt,mt)) by FINSEQ_2:144;
rng mt c= NAT by FINSEQ_1:def 4;
then A13: rng (mt * rt2) c= NAT by A8, XBOOLE_1:1;
set SS = Segm (Segm M,nt,mt),rt1,rt2;
A14: rng (nt * rt1) c= rng nt by RELAT_1:45;
rng nt c= NAT by FINSEQ_1:def 4;
then A15: rng (nt * rt1) c= NAT by A14, XBOOLE_1:1;
reconsider nr = nt * rt1, mr = mt * rt2 as FinSequence by A9, A11, FINSEQ_1:20;
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:110;
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 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 13;
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_1:25;
then A20: i in dom nr by A17, ZFMISC_1:106;
A21: j in dom mr by A17, A19, ZFMISC_1:106;
[i,j] in Indices (Segm M,nr,mr) by A17, MATRIX_1:27;
hence (Segm M,nr,mr) * i,j = M * (nr . I),(mr . J) by Def1
.= M * (nt . rtI),(mr . J) by A20, FUNCT_1:22
.= M * (nt . rtI),(mt . rtJ) by A21, FUNCT_1:22
.= (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_1:28;
[:(rng nr),(rng mr):] c= [:(rng nt),(rng mt):] by A14, A8, 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 A6, A22, Th76; :: thesis: verum

end;

end;