let n, m be Nat; :: thesis: for r being Real
for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
let r be Real; :: thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
let f be n -element real-valued FinSequence; :: thesis: for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
let M be Matrix of n,m,F_Real; :: thesis: (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)
set rf = r * f;
set T = Mx2Tran M;

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

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

per cases ( m = 0 or m > 0 ) ;

suppose A2: m = 0 ; :: thesis: (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)

then (Mx2Tran M) . (r * f) = 0.REAL 0 ;
hence (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f) by A2; :: thesis: verum

end;

suppose m > 0 ; :: thesis: (Mx2Tran M) . (r * f) = r * ((Mx2Tran M) . f)

reconsider R = r as Element of F_Real by XREAL_0:def 1;
set Lr = LineVec2Mx (@ (r * f));
set L = LineVec2Mx (@ f);
A3: R * (@ f) = @ (r * f) by MATRIXR1:17;
len f = n by CARD_1:def 7;
then A4: width (LineVec2Mx (@ f)) = n by MATRIX13:1;
A5: len M = n by A1, MATRIX13:1;
len (LineVec2Mx (@ f)) = 1 by MATRIX13:1;
then A6: len ((LineVec2Mx (@ f)) * M) = 1 by A4, A5, MATRIX_3:def 4;
(Mx2Tran M) . (@ f) = Line (((LineVec2Mx (@ f)) * M),1) by A1, Def3;
hence r * ((Mx2Tran M) . f) = R * (Line (((LineVec2Mx (@ f)) * M),1)) by MATRIXR1:17
.= Line ((R * ((LineVec2Mx (@ f)) * M)),1) by A6, MATRIXR1:20
.= Line (((R * (LineVec2Mx (@ f))) * M),1) by A4, A5, MATRIX15:1
.= Line (((LineVec2Mx (@ (r * f))) * M),1) by A3, MATRIX15:29
.= (Mx2Tran M) . (r * f) by A1, Def3 ;
:: thesis: verum

end;

end;

end;

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

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

end;

end;