let n, m be Nat; :: thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for P being Permutation of (Seg n) holds
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
let f be n -element real-valued FinSequence; :: thesis: for M being Matrix of n,m,F_Real
for P being Permutation of (Seg n) holds
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
let M be Matrix of n,m,F_Real; :: thesis: for P being Permutation of (Seg n) holds
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
let P be Permutation of (Seg n); :: thesis: ( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
A1: len f = n by CARD_1:def 7;
then A2: ( rng P = Seg n & dom f = Seg n ) by FINSEQ_1:def 3, FUNCT_2:def 3;
dom P = Seg n by FUNCT_2:52;
then A3: dom (f * P) = Seg n by A2, RELAT_1:27;
then reconsider fP = f * P as FinSequence by FINSEQ_1:def 2;
rng (f * P) = rng f by A2, RELAT_1:28;
then reconsider fP = fP as FinSequence of REAL by FINSEQ_1:def 4;
A4: len fP = n by A1, A3, FINSEQ_1:def 3;
then A5: fP is n -element by CARD_1:def 7;
(Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P)

proof

per cases ( n <> 0 or n = 0 ) ;

suppose A6: n <> 0 ; :: thesis: (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P)

then A7: width M = m by MATRIX13:1;
set MP = M * P;
A8: len M = n by A6, MATRIX13:1;

A9: now :: thesis: for i being Nat st 1 <= i & i <= m holds
((Mx2Tran (M * P)) . fP) . i = ((Mx2Tran M) . f) . i

let i be Nat; :: thesis: ( 1 <= i & i <= m implies ((Mx2Tran (M * P)) . fP) . i = ((Mx2Tran M) . f) . i )
assume A10: ( 1 <= i & i <= m ) ; :: thesis: ((Mx2Tran (M * P)) . fP) . i = ((Mx2Tran M) . f) . i
then i in Seg m ;
then A11: mlt ((@ fP),(Col ((M * P),i))) = the multF of F_Real .: (fP,((Col (M,i)) * P)) by A7, Th15
.= (mlt ((@ f),(Col (M,i)))) * P by FUNCOP_1:25 ;
len (Col (M,i)) = n by A8, CARD_1:def 7;
then len (mlt ((@ f),(Col (M,i)))) = n by A1, MATRIX_3:6;
then A12: dom (mlt ((@ f),(Col (M,i)))) = Seg n by FINSEQ_1:def 3;
((Mx2Tran (M * P)) . fP) . i = (@ fP) "*" (Col ((M * P),i)) by A6, A5, A10, Th18
.= the addF of F_Real "**" (mlt ((@ fP),(Col ((M * P),i)))) ;
hence ((Mx2Tran (M * P)) . fP) . i = (@ f) "*" (Col (M,i)) by A12, A11, FINSOP_1:7
.= ((Mx2Tran M) . f) . i by A6, A10, Th18 ;
:: thesis: verum

end;

( len ((Mx2Tran M) . f) = m & len ((Mx2Tran (M * P)) . fP) = m ) by A5, CARD_1:def 7;
hence (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) by A9; :: thesis: verum

end;

suppose A13: n = 0 ; :: thesis: (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P)

len fP = n by A4;
then card fP = n ;
then A14: fP is n -element FinSequence by CARD_1:def 7;
thus (Mx2Tran M) . f = 0. (TOP-REAL m) by Def3, A13
.= (Mx2Tran (M * P)) . fP by A13, Def3, A14
.= (Mx2Tran (M * P)) . (f * P) ; :: thesis: verum

end;

end;

end;

hence ( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL ) by A4, CARD_1:def 7; :: thesis: verum