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);
i in dom M by A1, FINSEQ_1:def 3;
then A3: M . i = (MX2FinS M) /. i by PARTFUN1:def 8;
len M = m by MATRIX_1:def 3;
then A4: Line M,i = M . i by A1, MATRIX_2:10;
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 8;
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_2:10;
hence Line (FinS2MX (L (#) (MX2FinS M))),i = a * ((MX2FinS M) /. i) by A2, A3, A6, VECTSP_6:def 8
.= a * L by A3, A4, Th102
.= a * (Line M,i) ;
:: thesis: verum