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 and
A2: card P = card Q and
A3: card P = the_rank_of M and
A4: Det (EqSegm M,P,Q) <> 0. K by Def4;
A5: [:Q,P:] c= Indices (M @ ) by A1, A2, Th69;
consider P1, Q1 being finite without_zero Subset of NAT such that
A6: [:P1,Q1:] c= Indices (M @ ) and
A7: card P1 = card Q1 and
A8: card P1 = the_rank_of (M @ ) and
A9: Det (EqSegm (M @ ),P1,Q1) <> 0. K by Def4;
A10: [:Q1,P1:] c= Indices M by A6, A7, Th69;
then Det (EqSegm M,Q1,P1) <> 0. K by A7, A9, Th70;
then A11: the_rank_of M >= the_rank_of (M @ ) by A7, A8, A10, Def4;
Det (EqSegm (M @ ),Q,P) <> 0. K by A1, A2, A4, Th70;
then the_rank_of (M @ ) >= the_rank_of M by A2, A3, A5, Def4;
hence the_rank_of M = the_rank_of (M @ ) by A11, XXREAL_0:1; :: thesis: verum