let n, m be Nat; :: thesis: for r being Real
for R being Element of F_Real
for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real st r = R holds
r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
let r be Real; :: thesis: for R being Element of F_Real
for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real st r = R holds
r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
let R be Element of F_Real; :: thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real st r = R holds
r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
let f be n -element real-valued FinSequence; :: thesis: for M being Matrix of n,m,F_Real st r = R holds
r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f
let M be Matrix of n,m,F_Real; :: thesis: ( r = R implies r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f )
set L = LineVec2Mx (@ f);
set RM = R * M;
set T = Mx2Tran M;
set TR = Mx2Tran (R * M);
assume A1: r = R ; :: thesis: r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f

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

suppose A2: n <> 0 ; :: thesis: r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f

A3: len M = n by A2, MATRIX13:1;
len f = n by CARD_1:def 7;
then A4: width (LineVec2Mx (@ f)) = n by MATRIX13:1;
len (LineVec2Mx (@ f)) = 1 by MATRIX13:1;
then A5: len ((LineVec2Mx (@ f)) * M) = 1 by A4, A3, MATRIX_3:def 4;
(Mx2Tran M) . f = Line (((LineVec2Mx (@ f)) * M),1) by A2, Def3;
hence r * ((Mx2Tran M) . f) = R * (Line (((LineVec2Mx (@ f)) * M),1)) by A1, MATRIXR1:17
.= Line ((R * ((LineVec2Mx (@ f)) * M)),1) by A5, MATRIXR1:20
.= Line (((LineVec2Mx (@ f)) * (R * M)),1) by A4, A3, MATRIXR1:22
.= (Mx2Tran (R * M)) . f by A2, Def3 ;
:: thesis: verum

end;

suppose A6: n = 0 ; :: thesis: r * ((Mx2Tran M) . f) = (Mx2Tran (R * M)) . f

A7: 0. (TOP-REAL m) = 0* m by EUCLID:70
.= m |-> 0 ;
hence r * ((Mx2Tran M) . f) = r * (m |-> zz) by A6, Def3
.= m |-> (r * zz) by RVSUM_1:48
.= (Mx2Tran (R * M)) . f by A6, A7, Def3 ;
:: thesis: verum

end;

end;