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 and
A3: card P = card Q and
A4: card P = RANK and
A5: Det (EqSegm (M,P,Q)) <> 0. K by Def4;
reconsider Sp = Sgm P, Sq = Sgm Q as Element of RANK -tuples_on NAT by A3, A4;
A6: rng Sp = P by FINSEQ_1:def 14;
A7: rng Sq = Q by FINSEQ_1:def 14;
EqSegm (M,P,Q) = Segm (M,P,Q) by A3, 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, A4, A5, A6, A7; :: 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
A8: [:(rng nt1),(rng nt2):] c= Indices M and
A9: Det (Segm (M,nt1,nt2)) <> 0. K ; :: thesis: n <= RANK
ex P1, P2 being finite without_zero Subset of NAT st
( P1 = rng nt1 & P2 = rng nt2 & card P1 = card P2 & card P1 = n & Det (EqSegm (M,P1,P2)) <> 0. K ) by A8, A9, Th75;
hence n <= RANK by A1, A8, Def4; :: thesis: verum

end;

assume that
A10: 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
A11: 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
A12: [:(rng rt1),(rng rt2):] c= Indices M and
A13: Det (Segm (M,rt1,rt2)) <> 0. K by A10;
consider P, Q being finite without_zero Subset of NAT such that
A14: [:P,Q:] c= Indices M and
A15: card P = card Q and
A16: card P = the_rank_of M and
A17: Det (EqSegm (M,P,Q)) <> 0. K by Def4;
ex P1, P2 being finite without_zero Subset of NAT st
( P1 = rng rt1 & P2 = rng rt2 & card P1 = card P2 & card P1 = RANK & Det (EqSegm (M,P1,P2)) <> 0. K ) by A12, A13, Th75;
then A18: RANK <= card P by A12, A16, Def4;
reconsider SP = Sgm P, SQ = Sgm Q as Element of (card P) -tuples_on NAT by A15;
A19: rng SP = P by FINSEQ_1:def 14;
A20: rng SQ = Q by FINSEQ_1:def 14;
EqSegm (M,P,Q) = Segm (M,P,Q) by A15, Def3
.= Segm (M,(Sgm P),(Sgm Q)) ;
then card P <= RANK by A11, A14, A15, A17, A19, A20;
hence the_rank_of M = RANK by A16, A18, XXREAL_0:1; :: thesis: verum