let m, n 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: card (Seg (len M)) = len M by FINSEQ_1:57;
A2: len M = n by MATRIX_0:def 2;
then reconsider F9 = F as Permutation of (Seg (card (Seg (len M)))) by A1;
A3: rng F = Seg n by FUNCT_2:def 3;
A4: dom F = Seg n by FUNCT_2:52;
A5: dom (Sgm (Seg (len M))) = Seg (card (Seg (len M))) by FINSEQ_3:40;
then A6: dom ((Sgm (Seg (len M))) * F) = dom F by A2, A1, A3, RELAT_1:27;
then reconsider SPF = (Sgm (Seg (len M))) * F as FinSequence by A4, FINSEQ_1:def 2;
A7: rng ((Sgm (Seg (len M))) * F) = rng (Sgm (Seg (len M))) by A2, A1, A5, A3, RELAT_1:28;
then reconsider SPF = SPF as FinSequence of NAT by FINSEQ_1:def 4;
len SPF = card (Seg (len M)) by A2, A1, A6, A4, FINSEQ_1:def 3;
then reconsider SPF = SPF as Element of (card (Seg (len M))) -tuples_on NAT by FINSEQ_2:92;
A8: Indices M = [:(Seg (len M)),(Seg (width M)):] by FINSEQ_1:def 3;
A9: rng (Sgm (Seg (width M))) = Seg (width M) by FINSEQ_1:def 14;
A10: rng (Sgm (Seg (len M))) = Seg (len M) by FINSEQ_1:def 14;
Segm (M,SPF,(Sgm (Seg (width M)))) = (Segm (M,(Seg (len M)),(Seg (width M)))) * F9 by Th33
.= M * F by Th46 ;
hence the_rank_of M = the_rank_of (M * F) by A7, A8, A10, A9, Th82; :: thesis: verum