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 A1: x in the carrier of V1 ; :: thesis: (Mx2Tran (a * A),b1,B2) . x = (a * (Mx2Tran A,b1,B2)) . x
reconsider v = x as Element of V1 by A1;
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;
A2: ( len (LineVec2Mx (v |-- b1)) = 1 & width (LineVec2Mx (v |-- b1)) = len (v |-- b1) & len (v |-- b1) = len b1 & len A = len b1 ) by MATRIX_1:24, MATRIX_1:def 3, MATRLIN:def 9;
then A3: len ((LineVec2Mx (v |-- b1)) * A) = 1 by MATRIX_3:def 4;
len (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)) = len (Line ((LineVec2Mx (v |-- b1)) * A),1) by MATRIXR1:16;
then A4: ( dom (lmlt (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)),B2) = (dom (a * (Line ((LineVec2Mx (v |-- b1)) * A),1))) /\ (dom B2) & dom (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)) = dom (Line ((LineVec2Mx (v |-- b1)) * A),1) & dom (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) = (dom (Line ((LineVec2Mx (v |-- b1)) * A),1)) /\ (dom B2) ) by Lm1, FINSEQ_3:31;
then A5: len (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) = len (lmlt (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)),B2) by FINSEQ_3:31;

A6: 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 A7: 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)
A8: ( k in dom (Line ((LineVec2Mx (v |-- b1)) * A),1) & k in dom (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)) & k in dom B2 ) by A7, A4, XBOOLE_0:def 4;
then A9: ( (Line ((LineVec2Mx (v |-- b1)) * A),1) . k = (Line ((LineVec2Mx (v |-- b1)) * A),1) /. k & B2 . k = B2 /. k & (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) . k = (lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) /. k ) by A7, PARTFUN1:def 8;
then A10: (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)) . k = a * ((Line ((LineVec2Mx (v |-- b1)) * A),1) /. k) by A8, FVSUM_1:62;
thus (lmlt (a * (Line ((LineVec2Mx (v |-- b1)) * A),1)),B2) . k = (a * ((Line ((LineVec2Mx (v |-- b1)) * A),1) /. k)) * (B2 /. k) by A4, A7, A9, A10, FUNCOP_1:28
.= a * (((Line ((LineVec2Mx (v |-- b1)) * A),1) /. k) * (B2 /. k)) by VECTSP_1:def 26
.= a * ((lmlt (Line ((LineVec2Mx (v |-- b1)) * A),1),B2) /. k) by A7, A9, 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 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 A5, A6, 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