let m, n, i 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);
set FLM = FinS2MX (L (#) (MX2FinS M));
( len (L (#) (MX2FinS M)) = len M & i in dom M & len M = m ) by A1, FINSEQ_1:def 3, MATRIX_1:def 3, VECTSP_6:def 8;
then A3: ( Line (FinS2MX (L (#) (MX2FinS M))),i = (FinS2MX (L (#) (MX2FinS M))) . i & M . i = (MX2FinS M) /. i & i in dom (FinS2MX (L (#) (MX2FinS M))) & Line M,i = M . i & Line M,i in lines M ) by A1, Th103, FINSEQ_1:def 3, MATRIX_2:10, PARTFUN1:def 8;
then reconsider L = Line M,i as Element of n -tuples_on the carrier of K by Th102;
thus Line (FinS2MX (L (#) (MX2FinS M))),i = a * ((MX2FinS M) /. i) by A2, A3, VECTSP_6:def 8
.= a * L by A3, Th102
.= a * (Line M,i) ; :: thesis: verum