theorem Th16: :: MATRTOP2:16

for n, m being Nat
for f being b₁ -element real-valued FinSequence
for M being Matrix of n,m,F_Real st M is without_repeated_line holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) )