let n, m be Nat; :: thesis:
let K be Field; :: thesis:
let nt be Element of n -tuples_on NAT ; :: thesis:
let mt be Element of m -tuples_on NAT ; :: thesis:
let M be Matrix of K; :: thesis:
set RM = the_rank_of M;
set S = Segm M,nt,mt;
consider rt1, rt2 being Element of (the_rank_of M) -tuples_on NAT such that
A1: [:(rng rt1),(rng rt2):] c= Indices M and
A2: Det (Segm M,rt1,rt2) <> 0. K by Th76;
assume A3: [:(rng nt),(rng mt):] = Indices M ; :: thesis:

A4: now

suppose the_rank_of M = 0 ; :: thesis:

hence the_rank_of M <= the_rank_of (Segm M,nt,mt) ; :: thesis:

end;

suppose A5: the_rank_of M > 0 ; :: thesis:

then len rt2 > 0 by FINSEQ_1:def 18;
then A6: rt2 <> {} ;
len rt1 > 0 by A5, FINSEQ_1:def 18;
then A7: rt1 <> {} ;
then rng nt <> {} by A3, A1, A6;
then dom nt <> {} by RELAT_1:65;
then B9: n <> 0 ;
then A10: width (Segm M,nt,mt) = m by Th1;
A11: dom mt = Seg m by FINSEQ_2:144;
set MR = Segm M,rt1,rt2;
A12: dom rt2 = Seg (the_rank_of M) by FINSEQ_2:144;
rng rt1 c= rng nt by A3, A1, A7, A6, ZFMISC_1:138;
then consider R1 being Function such that
A13: dom R1 = dom rt1 and
A14: rng R1 c= dom nt and
A15: rt1 = nt * R1 by Th81;
rng rt2 c= rng mt by A3, A1, A7, A6, ZFMISC_1:138;
then consider R2 being Function such that
A16: dom R2 = dom rt2 and
A17: rng R2 c= dom mt and
A18: rt2 = mt * R2 by Th81;
A19: dom rt1 = Seg (the_rank_of M) by FINSEQ_2:144;
then reconsider R1 = R1, R2 = R2 as FinSequence by A13, A16, A12, FINSEQ_1:def 2;
A20: rng R1 c= NAT by A14, XBOOLE_1:1;
rng R2 c= NAT by A17, XBOOLE_1:1;
then reconsider R1 = R1, R2 = R2 as FinSequence of NAT by A20, FINSEQ_1:def 4;
A21: len R1 = the_rank_of M by A13, A19, FINSEQ_1:def 3;
len R2 = the_rank_of M by A16, A12, FINSEQ_1:def 3;
then reconsider R1 = R1, R2 = R2 as Element of (the_rank_of M) -tuples_on NAT by A21, FINSEQ_2:110;
set SR = Segm (Segm M,nt,mt),R1,R2;
len (Segm M,nt,mt) = n by Th1, B9;
then A22: Indices (Segm M,nt,mt) = [:(Seg n),(Seg m):] by A10, FINSEQ_1:def 3;

A23: dom mt = Seg m by FINSEQ_2:144;
let i, j be Nat; :: thesis:
assume A24: [i,j] in Indices (Segm (Segm M,nt,mt),R1,R2) ; :: thesis:
reconsider I = i, J = j, RI = R1 . i, RJ = R2 . j as Element of NAT by ORDINAL1:def 13;
A25: dom nt = Seg n by FINSEQ_2:144;
A26: Indices (Segm (Segm M,nt,mt),R1,R2) = [:(dom R1),(dom R2):] by A13, A16, A19, A12, MATRIX_1:25;
then A27: i in dom R1 by A24, ZFMISC_1:106;
A28: j in dom R2 by A24, A26, ZFMISC_1:106;
then A29: R2 . j in rng R2 by FUNCT_1:def 5;
R1 . i in rng R1 by A27, FUNCT_1:def 5;
then A30: [(R1 . I),(R2 . J)] in Indices (Segm M,nt,mt) by A14, A17, A22, A29, A25, A23, ZFMISC_1:106;
[i,j] in Indices (Segm M,rt1,rt2) by A24, MATRIX_1:27;
hence (Segm M,rt1,rt2) * i,j = M * (rt1 . I),(rt2 . J) by Def1
.= M * (nt . RI),(rt2 . J) by A13, A15, A27, FUNCT_1:22
.= M * (nt . RI),(mt . RJ) by A16, A18, A28, FUNCT_1:22
.= (Segm M,nt,mt) * (R1 . I),(R2 . J) by A30, Def1
.= (Segm (Segm M,nt,mt),R1,R2) * i,j by A24, Def1 ;
:: thesis:

end;

then A31: Det (Segm (Segm M,nt,mt),R1,R2) <> 0. K by A2, MATRIX_1:28;
dom nt = Seg n by FINSEQ_2:144;
then [:(rng R1),(rng R2):] c= Indices (Segm M,nt,mt) by A14, A17, A11, A22, ZFMISC_1:119;
hence the_rank_of M <= the_rank_of (Segm M,nt,mt) by A31, Th76; :: thesis:

end;

end;

end;

the_rank_of M >= the_rank_of (Segm M,nt,mt) by A3, Th78;
hence the_rank_of M = the_rank_of (Segm M,nt,mt) by A4, XXREAL_0:1; :: thesis: