theorem Th107: :: MATRIX13:107

for i, m, n being Nat
for K being Field
for L being Linear_Combination of n -VectSp_over K
for M being Matrix of m,n,K st M is without_repeated_line & Carrier L c= lines M & i in Seg n holds
(Sum L) . i = Sum (Col ((FinS2MX (L (#) (MX2FinS M))),i))