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_0:23, MATRLIN:def 7;
A3: len M = len b1 by MATRIX_0:def 2;
then width M = 0 by A1, MATRIX_0:def 3;
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:43;
hence (Mx2Tran (M,b1,B2)) . v1 = 0. V2 by Def3; :: thesis: verum