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