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):] = 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);
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: the_rank_of M = the_rank_of (Segm (M,nt,mt))

A4: now :: thesis: the_rank_of M <= the_rank_of (Segm (M,nt,mt))

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 A5: the_rank_of M > 0 ; :: thesis: the_rank_of M <= the_rank_of (Segm (M,nt,mt))

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

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

A22: dom mt = Seg m by FINSEQ_2:124;
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 A23: [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 12;
A24: dom nt = Seg n by FINSEQ_2:124;
A25: Indices (Segm ((Segm (M,nt,mt)),R1,R2)) = [:(dom R1),(dom R2):] by A12, A15, A18, A11, MATRIX_0:24;
then A26: i in dom R1 by A23, ZFMISC_1:87;
A27: j in dom R2 by A23, A25, ZFMISC_1:87;
then A28: R2 . j in rng R2 by FUNCT_1:def 3;
R1 . i in rng R1 by A26, FUNCT_1:def 3;
then A29: [(R1 . I),(R2 . J)] in Indices (Segm (M,nt,mt)) by A13, A16, A21, A28, A24, A22, ZFMISC_1:87;
[i,j] in Indices (Segm (M,rt1,rt2)) by A23, MATRIX_0:26;
hence (Segm (M,rt1,rt2)) * (i,j) = M * ((rt1 . I),(rt2 . J)) by Def1
.= M * ((nt . RI),(rt2 . J)) by A12, A14, A26, FUNCT_1:12
.= M * ((nt . RI),(mt . RJ)) by A15, A17, A27, FUNCT_1:12
.= (Segm (M,nt,mt)) * ((R1 . I),(R2 . J)) by A29, Def1
.= (Segm ((Segm (M,nt,mt)),R1,R2)) * (i,j) by A23, Def1 ;
:: thesis: verum

end;

then A30: Det (Segm ((Segm (M,nt,mt)),R1,R2)) <> 0. K by A2, MATRIX_0:27;
dom nt = Seg n by FINSEQ_2:124;
then [:(rng R1),(rng R2):] c= Indices (Segm (M,nt,mt)) by A13, A16, A10, A21, ZFMISC_1:96;
hence the_rank_of M <= the_rank_of (Segm (M,nt,mt)) by A30, Th76; :: thesis: verum

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: verum