let K be Field; :: thesis: for a being Element of K
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for A being Matrix of len b1, len B2,K holds a * (Mx2Tran A,b1,B2) = Mx2Tran (a * A),b1,B2
let a be Element of K; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for A being Matrix of len b1, len B2,K holds a * (Mx2Tran A,b1,B2) = Mx2Tran (a * A),b1,B2
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for A being Matrix of len b1, len B2,K holds a * (Mx2Tran A,b1,B2) = Mx2Tran (a * A),b1,B2
let b1 be OrdBasis of V1; :: thesis: for B2 being FinSequence of V2
for A being Matrix of len b1, len B2,K holds a * (Mx2Tran A,b1,B2) = Mx2Tran (a * A),b1,B2
let B2 be FinSequence of V2; :: thesis: for A being Matrix of len b1, len B2,K holds a * (Mx2Tran A,b1,B2) = Mx2Tran (a * A),b1,B2
let A be Matrix of len b1, len B2,K; :: thesis: a * (Mx2Tran A,b1,B2) = Mx2Tran (a * A),b1,B2
set aA = a * A;
set aM = Mx2Tran (a * A),b1,B2;
set M = Mx2Tran A,b1,B2;

now

let x be set ; :: thesis: ( x in the carrier of V1 implies (Mx2Tran (a * A),b1,B2) . x = (a * (Mx2Tran A,b1,B2)) . x )
assume x in the carrier of V1 ; :: thesis: (Mx2Tran (a * A),b1,B2) . x = (a * (Mx2Tran A,b1,B2)) . x
then reconsider v = x as Element of V1 ;
set L = LineVec2Mx (v |-- b1);
set amA = lmlt (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)),B2;
set mA = lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2;
A1: ( width (LineVec2Mx (v |-- b1)) = len (v |-- b1) & len (v |-- b1) = len b1 ) by MATRIX_1:24, MATRLIN:def 9;
A2: len A = len b1 by MATRIX_1:def 3;
len (LineVec2Mx (v |-- b1)) = 1 by MATRIX_1:24;
then A3: len ((LineVec2Mx (v |-- b1)) * A) = 1 by A1, A2, MATRIX_3:def 4;
A4: dom (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) = (dom (Line ((LineVec2Mx (v |-- b1)) * A),1)) /\ (dom B2) by Lm1;
len (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)) = len (Line ((LineVec2Mx (v |-- b1)) * A),1) by MATRIXR1:16;
then A5: dom (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)) = dom (Line ((LineVec2Mx (v |-- b1)) * A),1) by FINSEQ_3:31;
A6: dom (lmlt (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)),B2) = (dom (a * (Line ((LineVec2Mx (v |-- b1)) * A),1))) /\ (dom B2) by Lm1;
then A7: len (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) = len (lmlt (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)),B2) by A5, A4, FINSEQ_3:31;

A8: now

let k be Element of NAT ; :: thesis: ( k in dom (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) implies (lmlt (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)),B2) . k = a * ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) /. k) )
assume A9: k in dom (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) ; :: thesis: (lmlt (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)),B2) . k = a * ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) /. k)
A10: (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) . k = (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) /. k by A9, PARTFUN1:def 8;
k in dom (Line ((LineVec2Mx (v |-- b1)) * A),1) by A4, A9, XBOOLE_0:def 4;
then A11: (Line ((LineVec2Mx (v |-- b1)) * A),1) . k = (Line ((LineVec2Mx (v |-- b1)) * A),1) /. k by PARTFUN1:def 8;
k in dom B2 by A4, A9, XBOOLE_0:def 4;
then A12: B2 . k = B2 /. k by PARTFUN1:def 8;
k in dom (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)) by A5, A4, A9, XBOOLE_0:def 4;
then (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)) . k = a * ((Line ((LineVec2Mx (v |-- b1)) * A),1) /. k) by A11, FVSUM_1:62;
hence (lmlt (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)),B2) . k = (a * ((Line ((LineVec2Mx (v |-- b1)) * A),1) /. k)) * (B2 /. k) by A6, A5, A4, A9, A12, FUNCOP_1:28
.= a * (((Line ((LineVec2Mx (v |-- b1)) * A),1) /. k) * (B2 /. k)) by VECTSP_1:def 28
.= a * ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) /. k) by A9, A11, A12, A10, FUNCOP_1:28 ;
:: thesis: verum

end;

thus (Mx2Tran (a * A),b1,B2) . x = Sum (lmlt (Line ((LineVec2Mx (v |-- b1)) * (a * A)),1),B2) by Def3
.= Sum (lmlt (Line (a * ((LineVec2Mx (v |-- b1)) * A)),1),B2) by A1, A2, MATRIXR1:22
.= Sum (lmlt (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)),B2) by A3, MATRIXR1:20
.= a * (Sum (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2)) by A7, A8, VECTSP_3:10
.= a * ((Mx2Tran A,b1,B2) . v) by Def3
.= (a * (Mx2Tran A,b1,B2)) . x by MATRLIN:def 6 ; :: thesis: verum

end;

hence a * (Mx2Tran A,b1,B2) = Mx2Tran (a * A),b1,B2 by FUNCT_2:18; :: thesis: verum