let n, m be Nat; :: thesis: for K being Field
for M being Matrix of n,m,K
for F being Permutation of (Seg n) holds the_rank_of M = the_rank_of (M * F)
let K be Field; :: thesis: for M being Matrix of n,m,K
for F being Permutation of (Seg n) holds the_rank_of M = the_rank_of (M * F)
let M be Matrix of n,m,K; :: thesis: for F being Permutation of (Seg n) holds the_rank_of M = the_rank_of (M * F)
let F be Permutation of (Seg n); :: thesis: the_rank_of M = the_rank_of (M * F)
set P = Seg (len M);
set Q = Seg (width M);
set SP = Sgm (Seg (len M));
set SQ = Sgm (Seg (width M));
A1: ( len M = n & card (Seg (len M)) = len M ) by FINSEQ_1:78, MATRIX_1:def 3;
then reconsider F' = F as Permutation of (Seg (card (Seg (len M)))) ;
( dom (Sgm (Seg (len M))) = Seg (card (Seg (len M))) & rng F = Seg n ) by FINSEQ_3:45, FUNCT_2:def 3;
then A2: ( dom ((Sgm (Seg (len M))) * F) = dom F & rng ((Sgm (Seg (len M))) * F) = rng (Sgm (Seg (len M))) & dom F = Seg n ) by A1, FUNCT_2:67, RELAT_1:46, RELAT_1:47;
then reconsider SPF = (Sgm (Seg (len M))) * F as FinSequence by FINSEQ_1:def 2;
reconsider SPF = SPF as FinSequence of NAT by A2, FINSEQ_1:def 4;
len SPF = card (Seg (len M)) by A1, A2, FINSEQ_1:def 3;
then reconsider SPF = SPF as Element of (card (Seg (len M))) -tuples_on NAT by FINSEQ_2:110;
A3: Segm M,SPF,(Sgm (Seg (width M))) = (Segm M,(Seg (len M)),(Seg (width M))) * F' by Th33
.= M * F by Th46 ;
( Indices M = [:(Seg (len M)),(Seg (width M)):] & rng (Sgm (Seg (len M))) = Seg (len M) & rng (Sgm (Seg (width M))) = Seg (width M) ) by FINSEQ_1:def 3, FINSEQ_1:def 13;
hence the_rank_of M = the_rank_of (M * F) by A2, A3, Th82; :: thesis: verum