let i, m, n be Nat; :: thesis: for K being Field
for a being Element of K
for L being Linear_Combination of n -VectSp_over K
for M being Matrix of m,n,K st i in Seg (len M) & a = L . (M . i) holds
Line ((FinS2MX (L (#) (MX2FinS M))),i) = a * (Line (M,i))
let K be Field; :: thesis: for a being Element of K
for L being Linear_Combination of n -VectSp_over K
for M being Matrix of m,n,K st i in Seg (len M) & a = L . (M . i) holds
Line ((FinS2MX (L (#) (MX2FinS M))),i) = a * (Line (M,i))
let a be Element of K; :: thesis: for L being Linear_Combination of n -VectSp_over K
for M being Matrix of m,n,K st i in Seg (len M) & a = L . (M . i) holds
Line ((FinS2MX (L (#) (MX2FinS M))),i) = a * (Line (M,i))
let L be Linear_Combination of n -VectSp_over K; :: thesis: for M being Matrix of m,n,K st i in Seg (len M) & a = L . (M . i) holds
Line ((FinS2MX (L (#) (MX2FinS M))),i) = a * (Line (M,i))
let M be Matrix of m,n,K; :: thesis: ( i in Seg (len M) & a = L . (M . i) implies Line ((FinS2MX (L (#) (MX2FinS M))),i) = a * (Line (M,i)) )
assume that
A1: i in Seg (len M) and
A2: a = L . (M . i) ; :: thesis: Line ((FinS2MX (L (#) (MX2FinS M))),i) = a * (Line (M,i))
set MX = MX2FinS M;
set LM = L (#) (MX2FinS M);
i in dom M by A1, FINSEQ_1:def 3;
then A3: M . i = (MX2FinS M) /. i by PARTFUN1:def 6;
len M = m by MATRIX_0:def 2;
then A4: Line (M,i) = M . i by A1, MATRIX_0:52;
then reconsider L = Line (M,i) as Element of n -tuples_on the carrier of K by A3, Th102;
set FLM = FinS2MX (L (#) (MX2FinS M));
A5: len (L (#) (MX2FinS M)) = len M by VECTSP_6:def 5;
then A6: i in dom (FinS2MX (L (#) (MX2FinS M))) by A1, FINSEQ_1:def 3;
Line ((FinS2MX (L (#) (MX2FinS M))),i) = (FinS2MX (L (#) (MX2FinS M))) . i by A1, A5, MATRIX_0:52;
hence Line ((FinS2MX (L (#) (MX2FinS M))),i) = a * ((MX2FinS M) /. i) by A2, A3, A6, VECTSP_6:def 5
.= a * L by A3, A4, Th102
.= a * (Line (M,i)) ;
:: thesis: verum