let K be Field; :: thesis: for M being Matrix of K
for RANK being Element of NAT holds
( the_rank_of M = RANK iff ( ex rt1, rt2 being Element of RANK -tuples_on NAT st
( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm M,rt1,rt2) <> 0. K ) & ( for n being Nat
for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm M,nt1,nt2) <> 0. K holds
n <= RANK ) ) )
let M be Matrix of K; :: thesis: for RANK being Element of NAT holds
( the_rank_of M = RANK iff ( ex rt1, rt2 being Element of RANK -tuples_on NAT st
( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm M,rt1,rt2) <> 0. K ) & ( for n being Nat
for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm M,nt1,nt2) <> 0. K holds
n <= RANK ) ) )
let RANK be Element of NAT ; :: thesis: ( the_rank_of M = RANK iff ( ex rt1, rt2 being Element of RANK -tuples_on NAT st
( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm M,rt1,rt2) <> 0. K ) & ( for n being Nat
for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm M,nt1,nt2) <> 0. K holds
n <= RANK ) ) )
thus ( the_rank_of M = RANK implies ( ex rt1, rt2 being Element of RANK -tuples_on NAT st
( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm M,rt1,rt2) <> 0. K ) & ( for n being Nat
for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm M,nt1,nt2) <> 0. K holds
n <= RANK ) ) ) :: thesis: ( ex rt1, rt2 being Element of RANK -tuples_on NAT st
( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm M,rt1,rt2) <> 0. K ) & ( for n being Nat
for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm M,nt1,nt2) <> 0. K holds
n <= RANK ) implies the_rank_of M = RANK )

proof

assume A1: the_rank_of M = RANK ; :: thesis: ( ex rt1, rt2 being Element of RANK -tuples_on NAT st
( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm M,rt1,rt2) <> 0. K ) & ( for n being Nat
for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm M,nt1,nt2) <> 0. K holds
n <= RANK ) )
then consider P, Q being finite without_zero Subset of NAT such that
A2: ( [:P,Q:] c= Indices M & card P = card Q & card P = RANK ) and
A3: Det (EqSegm M,P,Q) <> 0. K by Def4;
reconsider Sp = Sgm P, Sq = Sgm Q as Element of RANK -tuples_on NAT by A2;
consider k being Nat such that
A4: P c= Seg k by Th43;
consider m being Nat such that
A5: Q c= Seg m by Th43;
A6: ( rng Sp = P & rng Sq = Q ) by A4, A5, FINSEQ_1:def 13;
EqSegm M,P,Q = Segm M,P,Q by A2, Def3
.= Segm M,(Sgm P),(Sgm Q) ;
hence ex rt1, rt2 being Element of RANK -tuples_on NAT st
( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm M,rt1,rt2) <> 0. K ) by A2, A3, A6; :: thesis: for n being Nat
for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm M,nt1,nt2) <> 0. K holds
n <= RANK
let n be Nat; :: thesis: for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm M,nt1,nt2) <> 0. K holds
n <= RANK
let nt1, nt2 be Element of n -tuples_on NAT ; :: thesis: ( [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm M,nt1,nt2) <> 0. K implies n <= RANK )
assume that
A7: [:(rng nt1),(rng nt2):] c= Indices M and
A8: Det (Segm M,nt1,nt2) <> 0. K ; :: thesis: n <= RANK
consider P1, P2 being finite without_zero Subset of NAT such that
A9: ( P1 = rng nt1 & P2 = rng nt2 ) and
A10: ( card P1 = card P2 & card P1 = n ) and
A11: Det (EqSegm M,P1,P2) <> 0. K by A7, A8, Th75;
thus n <= RANK by A1, A7, A9, A10, A11, Def4; :: thesis: verum

end;

assume that
A12: ex rt1, rt2 being Element of RANK -tuples_on NAT st
( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm M,rt1,rt2) <> 0. K ) and
A13: for n being Nat
for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm M,nt1,nt2) <> 0. K holds
n <= RANK ; :: thesis: the_rank_of M = RANK
consider rt1, rt2 being Element of RANK -tuples_on NAT such that
A14: ( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm M,rt1,rt2) <> 0. K ) by A12;
consider P1, P2 being finite without_zero Subset of NAT such that
A15: ( P1 = rng rt1 & P2 = rng rt2 ) and
A16: ( card P1 = card P2 & card P1 = RANK ) and
A17: Det (EqSegm M,P1,P2) <> 0. K by A14, Th75;
consider P, Q being finite without_zero Subset of NAT such that
A18: ( [:P,Q:] c= Indices M & card P = card Q & card P = the_rank_of M ) and
A19: Det (EqSegm M,P,Q) <> 0. K by Def4;
reconsider SP = Sgm P, SQ = Sgm Q as Element of (card P) -tuples_on NAT by A18;
consider k being Nat such that
A20: P c= Seg k by Th43;
consider m being Nat such that
A21: Q c= Seg m by Th43;
EqSegm M,P,Q = Segm M,P,Q by A18, Def3
.= Segm M,(Sgm P),(Sgm Q) ;
then ( Det (EqSegm M,P,Q) = Det (Segm M,SP,SQ) & rng SP = P & rng SQ = Q ) by A18, A20, A21, FINSEQ_1:def 13;
then ( card P <= RANK & RANK <= card P ) by A13, A14, A15, A16, A17, A18, A19, Def4;
hence the_rank_of M = RANK by A18, XXREAL_0:1; :: thesis: verum