theorem Th20: :: DUALSP06:20

for X being RealNormSpace
for x being Point of X
for M being non empty Subspace of X
for F, K being FinSequence of the carrier of X
for G being FinSequence of REAL st len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) holds
Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M }