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);
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

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 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;

now

A23: dom mt = Seg m by FINSEQ_2:144;
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 A24: [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;
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: verum

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