theorem Th5: :: NDIFF11:5

for m being non zero Nat
for x being Element of REAL m ex s being FinSequence of REAL m st
( dom s = Seg m & ( for i being Nat st 1 <= i & i <= m holds
ex ei being Element of REAL m st
( ei = (reproj (i,(0* m))) . 1 & s . i = ((proj (i,m)) . x) * ei ) ) & Sum s = x )