theorem Th15: :: MATRTOP2:15

for n, m being Nat
for f being b₁ -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )