theorem Th8: :: BHSP_5:8

for X being RealUnitarySpace
for x being Point of X
for p being FinSequence of the carrier of X st len p >= 1 holds
for q being FinSequence of REAL st dom p = dom q & ( for i being Nat st i in dom q holds
q . i = the scalar of X . [x,(p . i)] ) holds
x .|. ( the addF of X "**" p) = addreal "**" q