let K be Field; :: thesis: for M being Matrix of K holds the_rank_of M = the_rank_of (M @ )
let M be Matrix of K; :: thesis: the_rank_of M = the_rank_of (M @ )
consider P, Q being finite without_zero Subset of NAT such that
A1: ( [:P,Q:] c= Indices M & card P = card Q ) and
A2: ( card P = the_rank_of M & Det (EqSegm M,P,Q) <> 0. K ) by Def4;
( [:Q,P:] c= Indices (M @ ) & Det (EqSegm (M @ ),Q,P) <> 0. K ) by A1, A2, Th69, Th70;
then A3: the_rank_of (M @ ) >= the_rank_of M by A1, A2, Def4;
consider P1, Q1 being finite without_zero Subset of NAT such that
A4: ( [:P1,Q1:] c= Indices (M @ ) & card P1 = card Q1 ) and
A5: ( card P1 = the_rank_of (M @ ) & Det (EqSegm (M @ ),P1,Q1) <> 0. K ) by Def4;
A6: [:Q1,P1:] c= Indices M by A4, Th69;
then Det (EqSegm M,Q1,P1) <> 0. K by A4, A5, Th70;
then the_rank_of M >= the_rank_of (M @ ) by A4, A5, A6, Def4;
hence the_rank_of M = the_rank_of (M @ ) by A3, XXREAL_0:1; :: thesis: verum