theorem Th106: :: MATRIX13:106

for i, m, n being Nat
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))