let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for v1 being Element of V1
for M being Matrix of len b1, len B2,K st len b1 = 0 holds
(Mx2Tran M,b1,B2) . v1 = 0. V2
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for v1 being Element of V1
for M being Matrix of len b1, len B2,K st len b1 = 0 holds
(Mx2Tran M,b1,B2) . v1 = 0. V2
let b1 be OrdBasis of V1; :: thesis: for B2 being FinSequence of V2
for v1 being Element of V1
for M being Matrix of len b1, len B2,K st len b1 = 0 holds
(Mx2Tran M,b1,B2) . v1 = 0. V2
let B2 be FinSequence of V2; :: thesis: for v1 being Element of V1
for M being Matrix of len b1, len B2,K st len b1 = 0 holds
(Mx2Tran M,b1,B2) . v1 = 0. V2
let v1 be Element of V1; :: thesis: for M being Matrix of len b1, len B2,K st len b1 = 0 holds
(Mx2Tran M,b1,B2) . v1 = 0. V2
let M be Matrix of len b1, len B2,K; :: thesis: ( len b1 = 0 implies (Mx2Tran M,b1,B2) . v1 = 0. V2 )
assume A1: len b1 = 0 ; :: thesis: (Mx2Tran M,b1,B2) . v1 = 0. V2
set L = LineVec2Mx (v1 |-- b1);
set LM = (LineVec2Mx (v1 |-- b1)) * M;
set LL = Line ((LineVec2Mx (v1 |-- b1)) * M),1;
A2: ( width (LineVec2Mx (v1 |-- b1)) = len (v1 |-- b1) & len (v1 |-- b1) = len b1 ) by MATRIX_1:24, MATRLIN:def 9;
A3: len M = len b1 by MATRIX_1:def 3;
then width M = 0 by A1, MATRIX_1:def 4;
then width ((LineVec2Mx (v1 |-- b1)) * M) = 0 by A2, A3, MATRIX_3:def 4;
then A4: dom (Line ((LineVec2Mx (v1 |-- b1)) * M),1) = {} ;
dom (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) = (dom (Line ((LineVec2Mx (v1 |-- b1)) * M),1)) /\ (dom B2) by Lm1;
then lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2 = <*> the carrier of V2 by A4;
then Sum (lmlt (Line ((LineVec2Mx (v1 |-- b1)) * M),1),B2) = 0. V2 by RLVECT_1:60;
hence (Mx2Tran M,b1,B2) . v1 = 0. V2 by Def3; :: thesis: verum