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):] = 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):] = 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):] = 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):] = 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):] = Indices M implies the_rank_of M = the_rank_of (Segm M,nt,mt) )
set RM = the_rank_of M;
set S = Segm M,nt,mt;
assume A1: [:(rng nt),(rng mt):] = Indices M ; :: thesis: the_rank_of M = the_rank_of (Segm M,nt,mt)
consider rt1, rt2 being Element of (the_rank_of M) -tuples_on NAT such that
A2: ( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm M,rt1,rt2) <> 0. K ) by Th76;

now

per cases ( the_rank_of M = 0 or the_rank_of M > 0 ) ;

suppose the_rank_of 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) ; :: thesis: verum

end;

suppose the_rank_of M > 0 ; :: thesis: the_rank_of M <= the_rank_of (Segm M,nt,mt)

then ( len rt1 > 0 & len rt2 > 0 ) by FINSEQ_1:def 18;
then ( rt1 <> {} & rt2 <> {} ) ;
then A3: ( rng rt1 <> {} & rng rt2 <> {} ) ;
then [:(rng rt1),(rng rt2):] <> {} ;
then A4: ( rng rt1 c= rng nt & rng rt2 c= rng mt ) by A1, A2, ZFMISC_1:138;
then consider R1 being Function such that
A5: ( dom R1 = dom rt1 & rng R1 c= dom nt & rt1 = nt * R1 ) by Th81;
consider R2 being Function such that
A6: ( dom R2 = dom rt2 & rng R2 c= dom mt & rt2 = mt * R2 ) by A4, Th81;
A7: ( dom rt1 = Seg (the_rank_of M) & dom rt2 = Seg (the_rank_of M) ) by FINSEQ_2:144;
then reconsider R1 = R1, R2 = R2 as FinSequence by A5, A6, FINSEQ_1:def 2;
A8: ( dom nt = Seg n & dom mt = Seg m ) by FINSEQ_2:144;
( rng R1 c= NAT & rng R2 c= NAT ) by A5, A6, XBOOLE_1:1;
then reconsider R1 = R1, R2 = R2 as FinSequence of NAT by FINSEQ_1:def 4;
( len R1 = the_rank_of M & len R2 = the_rank_of M ) by A5, A6, A7, FINSEQ_1:def 3;
then reconsider R1 = R1, R2 = R2 as Element of (the_rank_of M) -tuples_on NAT by FINSEQ_2:110;
rng nt <> {} by A3, A4;
then ( dom nt <> {} & dom nt = Seg n ) by FINSEQ_2:144, RELAT_1:65;
then ( len (Segm M,nt,mt) = n & width (Segm M,nt,mt) = m ) by Th1, FINSEQ_1:4;
then A9: Indices (Segm M,nt,mt) = [:(Seg n),(Seg m):] by FINSEQ_1:def 3;
set SR = Segm (Segm M,nt,mt),R1,R2;
set MR = Segm M,rt1,rt2;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm (Segm M,nt,mt),R1,R2) implies (Segm M,rt1,rt2) * i,j = (Segm (Segm M,nt,mt),R1,R2) * i,j )
assume A10: [i,j] in Indices (Segm (Segm M,nt,mt),R1,R2) ; :: thesis: (Segm M,rt1,rt2) * i,j = (Segm (Segm M,nt,mt),R1,R2) * i,j
reconsider I = i, J = j, RI = R1 . i, RJ = R2 . j as Element of NAT by ORDINAL1:def 13;
Indices (Segm (Segm M,nt,mt),R1,R2) = [:(dom R1),(dom R2):] by A5, A6, A7, MATRIX_1:25;
then A11: ( i in dom R1 & j in dom R2 & [i,j] in Indices (Segm M,rt1,rt2) ) by A10, MATRIX_1:27, ZFMISC_1:106;
then ( R1 . i in rng R1 & R2 . j in rng R2 ) by FUNCT_1:def 5;
then ( R1 . i in dom nt & R2 . j in dom mt & dom nt = Seg n & dom mt = Seg m ) by A5, A6, FINSEQ_2:144;
then A12: [(R1 . I),(R2 . J)] in Indices (Segm M,nt,mt) by A9, ZFMISC_1:106;
thus (Segm M,rt1,rt2) * i,j = M * (rt1 . I),(rt2 . J) by A11, Def1
.= M * (nt . RI),(rt2 . J) by A5, A11, FUNCT_1:22
.= M * (nt . RI),(mt . RJ) by A6, A11, FUNCT_1:22
.= (Segm M,nt,mt) * (R1 . I),(R2 . J) by A12, Def1
.= (Segm (Segm M,nt,mt),R1,R2) * i,j by A10, Def1 ; :: thesis: verum

end;

then ( Det (Segm (Segm M,nt,mt),R1,R2) <> 0. K & [:(rng R1),(rng R2):] c= Indices (Segm M,nt,mt) ) by A2, A5, A6, A8, A9, MATRIX_1:28, ZFMISC_1:119;
hence the_rank_of M <= the_rank_of (Segm M,nt,mt) by Th76; :: thesis: verum

end;

end;

end;

then ( the_rank_of M <= the_rank_of (Segm M,nt,mt) & the_rank_of M >= the_rank_of (Segm M,nt,mt) ) by A1, Th78;
hence the_rank_of M = the_rank_of (Segm M,nt,mt) by XXREAL_0:1; :: thesis: verum