theorem Th7: :: BHSP_5:7

for X being RealUnitarySpace
for p being FinSequence of the carrier of X st len p >= 1 & ( for i, j being Nat st i in dom p & j in dom p & i <> j holds
the scalar of X . [(p . i),(p . j)] = 0 ) 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 . [(p . i),(p . i)] ) holds
( the addF of X "**" p) .|. ( the addF of X "**" p) = addreal "**" q